Documentation

Mathlib.Init.Logic

theorem not_of_eq_false {p : Prop} (h : p = False) :
theorem cast_proof_irrel {α : Sort u_1} {β : Sort u_1} (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_1} {φ : α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_1} {φ : α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
    Equations
    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_1} (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_1} {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_1} {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_1} {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.

                    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 : ααα) :