Documentation

Mathlib.Init.Logic

Note about Mathlib/Init/ #

The files in Mathlib/Init are leftovers from the port from Mathlib3. (They contain content moved from lean3 itself that Mathlib needed but was not moved to lean4.)

We intend to move all the content of these files out into the main Mathlib directory structure. Contributions assisting with this are appreciated.

theorem not_of_eq_false {p : Prop} (h : p = False) :
theorem cast_proof_irrel {α : Sort u} {β : Sort u} (h₁ : α = β) (h₂ : α = β) (a : α) :
cast h₁ a = cast h₂ a
theorem eq_rec_heq {α : Sort u} {φ : αSort v} {a : α} {a' : α} (h : a = a') (p : φ a) :
HEq (Eq.recOn h p) p

Alias of eqRec_heq.

theorem heq_of_eq_rec_left {α : Sort u} {φ : αSort v} {a : α} {a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') (h₂ : ep₁ = p₂) :
HEq p₁ p₂
theorem heq_of_eq_rec_right {α : Sort u} {φ : αSort v} {a : α} {a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a' = a) (h₂ : p₁ = ep₂) :
HEq p₁ p₂
theorem of_heq_true {a : Prop} (h : HEq a True) :
a
theorem eq_rec_compose {α : Sort u} {β : Sort u} {φ : Sort u} (p₁ : β = φ) (p₂ : α = β) (a : α) :
Eq.recOn p₁ (Eq.recOn p₂ a) = Eq.recOn a
theorem heq_prop {P : Prop} {Q : Prop} (p : P) (q : Q) :
HEq p q
def Xor' (a : Prop) (b : Prop) :
Equations
Instances For
    theorem not_of_not_not_not {a : Prop} :
    ¬¬¬a¬a

    Alias of the forward direction of not_not_not.

    theorem and_true_iff (p : Prop) :
    theorem true_and_iff (p : Prop) :
    theorem false_or_iff (p : Prop) :
    theorem or_false_iff (p : Prop) :
    theorem not_or_of_not {a : Prop} {b : Prop} :
    ¬a¬b¬(a b)
    theorem iff_true_iff {a : Prop} :
    (a True) a
    theorem true_iff_iff {a : Prop} :
    (True a) a
    theorem iff_false_iff {a : Prop} :
    theorem false_iff_iff {a : Prop} :
    theorem iff_self_iff (a : Prop) :
    (a a) True
    def ExistsUnique {α : Sort u} (p : αProp) :
    Equations
    Instances For

      Checks to see that xs has only one binder.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        ∃! x : α, p x means that there exists a unique x in α such that p x. This is notation for ExistsUnique (fun (x : α) ↦ p x).

        This notation does not allow multiple binders like ∃! (x : α) (y : β), p x y as a shorthand for ∃! (x : α), ∃! (y : β), p x y since it is liable to be misunderstood. Often, the intended meaning is instead ∃! q : α × β, p q.1 q.2.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Pretty-printing for ExistsUnique, following the same pattern as pretty printing for Exists. However, it does not merge binders.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            ∃! x ∈ s, p x means ∃! x, x ∈ s ∧ p x, which is to say that there exists a unique x ∈ s such that p x. Similarly, notations such as ∃! x ≤ n, p n are supported, using any relation defined using the binder_predicate command.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem ExistsUnique.intro {α : Sort u} {p : αProp} (w : α) (h₁ : p w) (h₂ : ∀ (y : α), p yy = w) :
              ∃! x : α, p x
              theorem ExistsUnique.elim {α : Sort u} {p : αProp} {b : Prop} (h₂ : ∃! x : α, p x) (h₁ : ∀ (x : α), p x(∀ (y : α), p yy = x)b) :
              b
              theorem exists_unique_of_exists_of_unique {α : Sort u} {p : αProp} (hex : ∃ (x : α), p x) (hunique : ∀ (y₁ y₂ : α), p y₁p y₂y₁ = y₂) :
              ∃! x : α, p x
              theorem ExistsUnique.exists {α : Sort u} {p : αProp} :
              (∃! x : α, p x)∃ (x : α), p x
              theorem ExistsUnique.unique {α : Sort u} {p : αProp} (h : ∃! x : α, p x) {y₁ : α} {y₂ : α} (py₁ : p y₁) (py₂ : p y₂) :
              y₁ = y₂
              theorem existsUnique_congr {α : Sort u} {p : αProp} {q : αProp} (h : ∀ (a : α), p a q a) :
              (∃! a : α, p a) ∃! a : α, q a
              def Decidable.recOn_true (p : Prop) [h : Decidable p] {h₁ : pSort u} {h₂ : ¬pSort u} (h₃ : p) (h₄ : h₁ h₃) :
              Decidable.recOn h h₂ h₁
              Equations
              Instances For
                def Decidable.recOn_false (p : Prop) [h : Decidable p] {h₁ : pSort u} {h₂ : ¬pSort u} (h₃ : ¬p) (h₄ : h₂ h₃) :
                Decidable.recOn h h₂ h₁
                Equations
                Instances For
                  def Decidable.by_cases {p : Prop} {q : Sort u} [dec : Decidable p] (h1 : pq) (h2 : ¬pq) :
                  q

                  Alias of Decidable.byCases.


                  Synonym for dite (dependent if-then-else). We can construct an element q (of any sort, not just a proposition) by cases on whether p is true or false, provided p is decidable.

                  Equations
                  Instances For
                    theorem Decidable.by_contradiction {p : Prop} [dec : Decidable p] (h : ¬pFalse) :
                    p

                    Alias of Decidable.byContradiction.

                    @[deprecated Decidable.not_not]

                    Alias of Decidable.not_not.

                    def Or.decidable {p : Prop} {q : Prop} [dp : Decidable p] [dq : Decidable q] :

                    Alias of instDecidableOr.

                    Equations
                    Instances For
                      def And.decidable {p : Prop} {q : Prop} [dp : Decidable p] [dq : Decidable q] :

                      Alias of instDecidableAnd.

                      Equations
                      Instances For
                        def Iff.decidable {p : Prop} {q : Prop} [Decidable p] [Decidable q] :

                        Alias of instDecidableIff.

                        Equations
                        Instances For
                          def IsDecEq {α : Sort u} (p : ααBool) :
                          Equations
                          Instances For
                            def IsDecRefl {α : Sort u} (p : ααBool) :
                            Equations
                            Instances For
                              def decidableEq_of_bool_pred {α : Sort u} {p : ααBool} (h₁ : IsDecEq p) (h₂ : IsDecRefl p) :
                              Equations
                              Instances For
                                theorem decidableEq_inl_refl {α : Sort u} [h : DecidableEq α] (a : α) :
                                h a a = isTrue
                                theorem decidableEq_inr_neg {α : Sort u} [h : DecidableEq α] {a : α} {b : α} (n : a b) :
                                h a b = isFalse n
                                theorem rec_subsingleton {p : Prop} [h : Decidable p] {h₁ : pSort u} {h₂ : ¬pSort u} [h₃ : ∀ (h : p), Subsingleton (h₁ h)] [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)] :
                                theorem imp_of_if_pos {c : Prop} {t : Prop} {e : Prop} [Decidable c] (h : if c then t else e) (hc : c) :
                                t
                                theorem imp_of_if_neg {c : Prop} {t : Prop} {e : Prop} [Decidable c] (h : if c then t else e) (hnc : ¬c) :
                                e
                                theorem if_ctx_congr {α : Sort u} {b : Prop} {c : Prop} [dec_b : Decidable b] [dec_c : Decidable c] {x : α} {y : α} {u : α} {v : α} (h_c : b c) (h_t : cx = u) (h_e : ¬cy = v) :
                                (if b then x else y) = if c then u else v
                                theorem if_congr {α : Sort u} {b : Prop} {c : Prop} [Decidable b] [Decidable c] {x : α} {y : α} {u : α} {v : α} (h_c : b c) (h_t : x = u) (h_e : y = v) :
                                (if b then x else y) = if c then u else v
                                theorem if_ctx_congr_prop {b : Prop} {c : Prop} {x : Prop} {y : Prop} {u : Prop} {v : Prop} [dec_b : Decidable b] [dec_c : Decidable c] (h_c : b c) (h_t : c(x u)) (h_e : ¬c(y v)) :
                                (if b then x else y) if c then u else v
                                theorem if_congr_prop {b : Prop} {c : Prop} {x : Prop} {y : Prop} {u : Prop} {v : Prop} [Decidable b] [Decidable c] (h_c : b c) (h_t : x u) (h_e : y v) :
                                (if b then x else y) if c then u else v
                                theorem if_ctx_simp_congr_prop {b : Prop} {c : Prop} {x : Prop} {y : Prop} {u : Prop} {v : Prop} [Decidable b] (h_c : b c) (h_t : c(x u)) (h_e : ¬c(y v)) :
                                (if b then x else y) if c then u else v
                                theorem if_simp_congr_prop {b : Prop} {c : Prop} {x : Prop} {y : Prop} {u : Prop} {v : Prop} [Decidable b] (h_c : b c) (h_t : x u) (h_e : y v) :
                                (if b then x else y) if c then u else v
                                theorem dif_ctx_congr {α : Sort u} {b : Prop} {c : Prop} [dec_b : Decidable b] [dec_c : Decidable c] {x : bα} {u : cα} {y : ¬bα} {v : ¬cα} (h_c : b c) (h_t : ∀ (h : c), x = u h) (h_e : ∀ (h : ¬c), y = v h) :
                                dite b x y = dite c u v
                                theorem dif_ctx_simp_congr {α : Sort u} {b : Prop} {c : Prop} [Decidable b] {x : bα} {u : cα} {y : ¬bα} {v : ¬cα} (h_c : b c) (h_t : ∀ (h : c), x = u h) (h_e : ∀ (h : ¬c), y = v h) :
                                dite b x y = dite c u v
                                def AsTrue (c : Prop) [Decidable c] :
                                Equations
                                Instances For
                                  def AsFalse (c : Prop) [Decidable c] :
                                  Equations
                                  Instances For
                                    theorem AsTrue.get {c : Prop} [h₁ : Decidable c] :
                                    AsTrue cc
                                    theorem let_value_eq {α : Sort u} {β : Sort v} {a₁ : α} {a₂ : α} (b : αβ) (h : a₁ = a₂) :
                                    (let x := a₁; b x) = let x := a₂; b x
                                    theorem let_value_heq {α : Sort v} {β : αSort u} {a₁ : α} {a₂ : α} (b : (x : α) → β x) (h : a₁ = a₂) :
                                    HEq (let x := a₁; b x) (let x := a₂; b x)
                                    theorem let_body_eq {α : Sort v} {β : αSort u} (a : α) {b₁ : (x : α) → β x} {b₂ : (x : α) → β x} (h : ∀ (x : α), b₁ x = b₂ x) :
                                    (let x := a; b₁ x) = let x := a; b₂ x
                                    theorem let_eq {α : Sort v} {β : Sort u} {a₁ : α} {a₂ : α} {b₁ : αβ} {b₂ : αβ} (h₁ : a₁ = a₂) (h₂ : ∀ (x : α), b₁ x = b₂ x) :
                                    (let x := a₁; b₁ x) = let x := a₂; b₂ x
                                    def Reflexive {β : Sort v} (r : ββProp) :

                                    A reflexive relation relates every element to itself.

                                    Equations
                                    Instances For
                                      def Symmetric {β : Sort v} (r : ββProp) :

                                      A relation is symmetric if x ≺ y implies y ≺ x.

                                      Equations
                                      Instances For
                                        def Transitive {β : Sort v} (r : ββProp) :

                                        A relation is transitive if x ≺ y and y ≺ z together imply x ≺ z.

                                        Equations
                                        • Transitive r = ∀ ⦃x y z : β⦄, r x yr y zr x z
                                        Instances For
                                          theorem Equivalence.reflexive {β : Sort v} {r : ββProp} (h : Equivalence r) :
                                          theorem Equivalence.symmetric {β : Sort v} {r : ββProp} (h : Equivalence r) :
                                          theorem Equivalence.transitive {β : Sort v} {r : ββProp} (h : Equivalence r) :
                                          def Total {β : Sort v} (r : ββProp) :

                                          A relation is total if for all x and y, either x ≺ y or y ≺ x.

                                          Equations
                                          Instances For
                                            def Irreflexive {β : Sort v} (r : ββProp) :

                                            Irreflexive means "not reflexive".

                                            Equations
                                            Instances For
                                              def AntiSymmetric {β : Sort v} (r : ββProp) :

                                              A relation is antisymmetric if x ≺ y and y ≺ x together imply that x = y.

                                              Equations
                                              Instances For
                                                def EmptyRelation {α : Sort u} :
                                                ααProp

                                                An empty relation does not relate any elements.

                                                Equations
                                                Instances For
                                                  theorem InvImage.trans {α : Sort u} {β : Sort v} (r : ββProp) (f : αβ) (h : Transitive r) :
                                                  theorem InvImage.irreflexive {α : Sort u} {β : Sort v} (r : ββProp) (f : αβ) (h : Irreflexive r) :
                                                  def Commutative {α : Type u} (f : ααα) :
                                                  Equations
                                                  Instances For
                                                    def Associative {α : Type u} (f : ααα) :
                                                    Equations
                                                    Instances For
                                                      def LeftIdentity {α : Type u} (f : ααα) (one : α) :
                                                      Equations
                                                      Instances For
                                                        def RightIdentity {α : Type u} (f : ααα) (one : α) :
                                                        Equations
                                                        Instances For
                                                          def RightInverse {α : Type u} (f : ααα) (inv : αα) (one : α) :
                                                          Equations
                                                          Instances For
                                                            def LeftCancelative {α : Type u} (f : ααα) :
                                                            Equations
                                                            Instances For
                                                              def RightCancelative {α : Type u} (f : ααα) :
                                                              Equations
                                                              Instances For
                                                                def LeftDistributive {α : Type u} (f : ααα) (g : ααα) :
                                                                Equations
                                                                Instances For
                                                                  def RightDistributive {α : Type u} (f : ααα) (g : ααα) :
                                                                  Equations
                                                                  Instances For
                                                                    def RightCommutative {α : Type u} {β : Type v} (h : βαβ) :
                                                                    Equations
                                                                    Instances For
                                                                      def LeftCommutative {α : Type u} {β : Type v} (h : αββ) :
                                                                      Equations
                                                                      • LeftCommutative h = ∀ (a₁ a₂ : α) (b : β), h a₁ (h a₂ b) = h a₂ (h a₁ b)
                                                                      Instances For
                                                                        theorem left_comm {α : Type u} (f : ααα) :
                                                                        theorem right_comm {α : Type u} (f : ααα) :