book/TPiL/AxiomsComputation.lean

GitHub source file

108 declarations, 0 contain sorry, 8 declared as axioms

1. inductive types, line 14 source
2. example (example at line 36) line 36 source
3. axiom Hidden.propext line 177 source

   Source comment

   ----

   axiom propext {a b : Prop} : (a ↔ b) → a = b
   ------
   end Hidden
   ```
   
   :::setup
   ```
   variable (a : Prop)
   ```
   It asserts that when two propositions imply one another, they are
   actually equal. This is consistent with set-theoretic interpretations
   in which any element {lean}`a : Prop` is either empty or the singleton set
   …

   Mentions: b, Hidden.is, in, Hidden.or

4. theorem thm₁ line 197 source
5. theorem thm₂ line 200 source
6. def Set line 278 source

   Also declared: examples/Examples/InteractExample7dtboffggkdqb.lean:2 (same declaration text).

7. def Set.mem line 282 source
8. theorem Set.setext line 286 source
9. example (example at line 294) line 294 source
10. def Set line 297 source

    Also declared: examples/Examples/InteractExample7dtboffggkdqb.lean:2 (same declaration text).

11. def Set.mem line 299 source
12. theorem Set.setext line 301 source
13. def Set.empty line 304 source

    Source comment

    ----

    def empty : Set α := fun _ => False
    …

    Mentions: Set, α

14. def Set.inter line 308 source
15. theorem Set.inter_self line 313 source
16. theorem Set.inter_empty line 318 source
17. theorem Set.empty_inter line 323 source
18. theorem Set.inter.comm line 328 source
19. def f line 340 source

    Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:416 (different declaration text), book/TPiL/InductionAndRecursion.lean:833 (different declaration text), book/TPiL/InteractingWithLean.lean:468 (different declaration text), book/TPiL/Tactics.lean:1457 (different declaration text). Qualify references as f@path.

20. def g line 341 source

    Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:417 (different declaration text), book/TPiL/Tactics.lean:1781 (different declaration text). Qualify references as g@path.

21. theorem f_eq_g line 343 source
22. def val line 346 source
23. theorem tteq line 370 source
24. def val line 373 source
25. axiom Hidden.Quot line 433 source
26. axiom Hidden.Quot.mk line 435 source
27. axiom Hidden.Quot.ind line 437 source
28. axiom Hidden.Quot.lift line 441 source
29. def mod7Rel line 467 source
30. def f line 476 source

    Distinct definitions of this name: book/TPiL/DependentTypeTheory.lean:416 (different declaration text), book/TPiL/InductionAndRecursion.lean:833 (different declaration text), book/TPiL/InteractingWithLean.lean:468 (different declaration text), book/TPiL/Tactics.lean:1457 (different declaration text). Qualify references as f@path.

31. theorem f_respects line 479 source
32. example (example at line 486) line 486 source

    Source comment

    the computation principle

    example (a : Nat) : Quot.lift f f_respects (Quot.mk mod7Rel a) = f a :=
    …

    Mentions: f_respects, mod7Rel

33. axiom Hidden.Quot.sound line 525 source

    Source comment

    ----

    axiom Quot.sound :
          ∀ {α : Type u} {r : α → α → Prop} {a b : α},
            r a b → Quot.mk r a = Quot.mk r b
    ```
    
    This is the axiom that asserts that any two elements of {leanRef}`α` that are
    related by {leanRef}`r` become identified in the quotient. If a theorem or
    definition makes use of {leanRef}`Quot.sound`, it will show up in the
    {kw}`#print axioms` command.
    
    :::setup
    ```
    …

    Mentions: α, b, Hidden.Quot.mk, Hidden.is, Hidden.of, in, Hidden.or

34. class Hidden.Hidden.Setoid line 561 source

    Source comment

    ----

    class Setoid (α : Sort u) where
    …

    Mentions: α

35. instance Hidden.Hidden.(instance at line 565) line 565 source
36. theorem Hidden.Hidden.Setoid.refl line 572 source
37. theorem Hidden.Hidden.Setoid.symm line 575 source
38. theorem Hidden.Hidden.Setoid.trans line 578 source
39. instance Hidden.of line 589 source
40. def Hidden.Hidden.Quotient line 594 source

    Source comment

    ----

    def Quotient {α : Sort u} (s : Setoid α) :=
    …

    Mentions: α, Hidden.Hidden.Setoid

41. theorem Hidden.(theorem at line 615) line 615 source
42. def Hidden.eqv line 641 source
43. def Hidden.eqv line 655 source
44. theorem Hidden.eqv.refl line 659 source

    Source comment

    ----

    private theorem eqv.refl (p : α × α) : p ~ p :=
    …

    Mentions: α

45. theorem Hidden.eqv.symm line 662 source
46. theorem Hidden.eqv.trans line 668 source
47. theorem Hidden.is_equivalence line 678 source
48. def Hidden.eqv line 688 source
49. theorem Hidden.eqv.refl line 691 source
50. theorem Hidden.eqv.symm line 693 source
51. theorem Hidden.eqv.trans line 698 source
52. theorem Hidden.is_equivalence line 707 source
53. instance Hidden.uprodSetoid line 710 source

    Source comment

    ----

    instance uprodSetoid (α : Type u) : Setoid (α × α) where
    …

    Mentions: α

54. def Hidden.UProd line 714 source
55. def Hidden.UProd.mk line 719 source
56. def Hidden.eqv line 730 source
57. theorem Hidden.eqv.refl line 733 source
58. theorem Hidden.eqv.symm line 735 source
59. theorem Hidden.eqv.trans line 740 source
60. theorem Hidden.is_equivalence line 749 source
61. instance Hidden.uprodSetoid line 752 source
62. def Hidden.UProd line 756 source
63. def Hidden.UProd.mk line 761 source
64. def Hidden.eqv line 783 source
65. theorem Hidden.eqv.refl line 786 source
66. theorem Hidden.eqv.symm line 788 source
67. theorem Hidden.eqv.trans line 793 source
68. theorem Hidden.is_equivalence line 802 source
69. instance Hidden.uprodSetoid line 804 source
70. def Hidden.UProd line 807 source
71. def Hidden.UProd.mk line 810 source
72. theorem Hidden.UProd.mk_eq_mk line 814 source

    Source comment

    ----

    theorem mk_eq_mk (a₁ a₂ : α) : {a₁, a₂} = {a₂, a₁} :=
    …

    Mentions: α

73. def Hidden.eqv line 831 source
74. theorem Hidden.eqv.refl line 834 source
75. theorem Hidden.eqv.symm line 836 source
76. theorem Hidden.eqv.trans line 841 source
77. theorem Hidden.is_equivalence line 850 source
78. instance Hidden.uprodSetoid line 852 source
79. def Hidden.UProd line 855 source
80. def Hidden.UProd.mk line 858 source
81. theorem Hidden.UProd.mk_eq_mk line 861 source
82. def Hidden.UProd.mem_fn line 864 source

    Source comment

    ----

    private def mem_fn (a : α) : α × α → Prop
      | (a₁, a₂) => a = a₁ ∨ a = a₂
    
    -- auxiliary lemma for proving mem_respects

    Mentions: α, Hidden.UProd.mem_respects

83. theorem Hidden.UProd.mem_swap auxiliary lemma for proving mem_respects line 868 source

    Source comment

    auxiliary lemma for proving mem_respects

    private theorem mem_swap {a : α} :
          ∀ {p : α × α}, mem_fn a p = mem_fn a (⟨p.2, p.1⟩)
      | (a₁, a₂) => by
        apply propext
        apply Iff.intro
        . intro
          | Or.inl h => exact Or.inr h
          | Or.inr h => exact Or.inl h
        . intro
          | Or.inl h => exact Or.inr h
          | Or.inr h => exact Or.inl h

    Mentions: α, Hidden.UProd.mem_fn, Hidden.propext

84. theorem Hidden.UProd.mem_respects line 880 source
85. def Hidden.UProd.mem line 887 source
86. theorem Hidden.UProd.mem_mk_left line 892 source
87. theorem Hidden.UProd.mem_mk_right line 895 source
88. theorem Hidden.UProd.mem_or_mem_of_mem_mk line 898 source
89. def Hidden.extfun line 913 source
90. def Hidden.extfun_app line 915 source
91. def Hidden.extfun line 935 source
92. def Hidden.extfun_app line 937 source
93. example Hidden.(example at line 940) line 940 source

    Source comment

    --------

    example (f₁ f₂ : (x : α) → β x) (h : ∀ x, f₁ x = f₂ x) :=
    …

    Mentions: x, α, β

94. class inductive Hidden.Hidden.Nonempty line 964 source

    Source comment

    ----

    class inductive Nonempty (α : Sort u) : Prop where
    …

    Mentions: α

95. example Hidden.(example at line 981) line 981 source
96. axiom Hidden.Hidden.choice line 991 source

    Source comment

    ----

    axiom choice {α : Sort u} : Nonempty α → α
    ------
    end Hidden
    ```
    
    :::setup
    ```
    variable {α : Sort u} {h : Nonempty α}
    open Classical
    ```
    
    Given only the assertion {lean}`h` that {lean}`α` is nonempty, {lean}`choice h`
    …

    Mentions: α, Hidden.Hidden.Nonempty, Hidden.is

97. theorem Hidden.is line 1010 source
98. axiom Hidden.Hidden.choice line 1017 source
99. def Hidden.Hidden.indefiniteDescription line 1019 source

    Source comment

    ----

    noncomputable def indefiniteDescription {α : Sort u}
        (p : α → Prop) (h : ∃ x, p x) : {x // p x} :=
    …

    Mentions: α, x

100. def Hidden.Hidden.choose line 1045 source
101. theorem Hidden.Hidden.choose_spec line 1048 source
102. def Hidden.inhabited_of_nonempty line 1061 source

     Source comment

     ----

     noncomputable def inhabited_of_nonempty (h : Nonempty α) : Inhabited α :=
     …

     Mentions: α

103. theorem Hidden.em line 1122 source
104. theorem Hidden.em line 1174 source
105. theorem Hidden.propComplete line 1252 source
106. class inductive Hidden.Hidden.Decidable line 1267 source

     Source comment

     ----

     class inductive Decidable (p : Prop) where
     …

107. def Hidden.linv line 1301 source
108. theorem Hidden.linv_comp_self line 1304 source