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.

@[deprecated Std.Commutative]
def Commutative {α : Type u} (f : ααα) :
Equations
Instances For
    @[deprecated Std.Associative]
    def Associative {α : Type u} (f : ααα) :
    Equations
    Instances For
      @[deprecated]
      def LeftIdentity {α : Type u} (f : ααα) (one : α) :
      Equations
      Instances For
        @[deprecated]
        def RightIdentity {α : Type u} (f : ααα) (one : α) :
        Equations
        Instances For
          @[deprecated]
          def RightInverse {α : Type u} (f : ααα) (inv : αα) (one : α) :
          Equations
          Instances For
            @[deprecated]
            def LeftCancelative {α : Type u} (f : ααα) :
            Equations
            Instances For
              @[deprecated]
              def RightCancelative {α : Type u} (f : ααα) :
              Equations
              Instances For
                @[deprecated]
                def LeftDistributive {α : Type u} (f : ααα) (g : ααα) :
                Equations
                Instances For
                  @[deprecated]
                  def RightDistributive {α : Type u} (f : ααα) (g : ααα) :
                  Equations
                  Instances For
                    @[deprecated of_eq_false]
                    theorem not_of_eq_false {p : Prop} (h : p = False) :

                    Alias of of_eq_false.

                    @[deprecated]
                    theorem cast_proof_irrel {α : Sort u} {β : Sort u} (h₁ : α = β) (h₂ : α = β) (a : α) :
                    cast h₁ a = cast h₂ a
                    @[deprecated eqRec_heq]
                    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.

                    @[deprecated proof_irrel_heq]
                    theorem heq_prop {p : Prop} {q : Prop} (hp : p) (hq : q) :
                    HEq hp hq

                    Alias of proof_irrel_heq.

                    @[deprecated]
                    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₂
                    @[deprecated]
                    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₂
                    @[deprecated]
                    theorem of_heq_true {a : Prop} (h : HEq a True) :
                    a
                    @[deprecated]
                    theorem eq_rec_compose {α : Sort u} {β : Sort u} {φ : Sort u} (p₁ : β = φ) (p₂ : α = β) (a : α) :
                    Eq.recOn p₁ (Eq.recOn p₂ a) = Eq.recOn a
                    @[deprecated not_not_not]
                    theorem not_of_not_not_not {a : Prop} :
                    ¬¬¬a¬a

                    Alias of the forward direction of not_not_not.

                    @[deprecated and_true]
                    theorem and_true_iff (p : Prop) :
                    @[deprecated true_and]
                    theorem true_and_iff (p : Prop) :
                    @[deprecated and_false]
                    theorem and_false_iff (p : Prop) :
                    @[deprecated false_and]
                    theorem false_and_iff (p : Prop) :
                    @[deprecated or_true]
                    theorem or_true_iff (p : Prop) :
                    @[deprecated true_or]
                    theorem true_or_iff (p : Prop) :
                    @[deprecated or_false]
                    theorem or_false_iff (p : Prop) :
                    @[deprecated false_or]
                    theorem false_or_iff (p : Prop) :
                    @[deprecated iff_true]
                    theorem iff_true_iff {a : Prop} :
                    (a True) a
                    @[deprecated true_iff]
                    theorem true_iff_iff {a : Prop} :
                    (True a) a
                    @[deprecated iff_false]
                    theorem iff_false_iff {a : Prop} :
                    @[deprecated false_iff]
                    theorem false_iff_iff {a : Prop} :
                    @[deprecated iff_self]
                    theorem iff_self_iff (a : Prop) :
                    (a a) True
                    @[deprecated not_or_intro]
                    theorem not_or_of_not {a : Prop} {b : Prop} (ha : ¬a) (hb : ¬b) :
                    ¬(a b)

                    Alias of not_or_intro.

                    @[deprecated]
                    @[deprecated]
                    @[deprecated]
                    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
                      @[deprecated]
                      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
                        @[deprecated Decidable.byCases]
                        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
                          @[deprecated Decidable.byContradiction]
                          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.

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

                          Alias of instDecidableOr.

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

                            Alias of instDecidableAnd.

                            Equations
                            Instances For
                              @[deprecated instDecidableNot]
                              def Not.decidable {p : Prop} [dp : Decidable p] :

                              Alias of instDecidableNot.

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

                                Alias of instDecidableIff.

                                Equations
                                Instances For
                                  @[deprecated instDecidableTrue]

                                  Alias of instDecidableTrue.

                                  Equations
                                  Instances For
                                    @[deprecated instDecidableFalse]

                                    Alias of instDecidableFalse.

                                    Equations
                                    Instances For
                                      @[deprecated]
                                      def IsDecEq {α : Sort u} (p : ααBool) :
                                      Equations
                                      Instances For
                                        @[deprecated]
                                        def IsDecRefl {α : Sort u} (p : ααBool) :
                                        Equations
                                        Instances For
                                          @[deprecated]
                                          def decidableEq_of_bool_pred {α : Sort u} {p : ααBool} (h₁ : IsDecEq p) (h₂ : IsDecRefl p) :
                                          Equations
                                          Instances For
                                            @[deprecated]
                                            theorem decidableEq_inl_refl {α : Sort u} [h : DecidableEq α] (a : α) :
                                            h a a = isTrue
                                            @[deprecated]
                                            theorem decidableEq_inr_neg {α : Sort u} [h : DecidableEq α] {a : α} {b : α} (n : a b) :
                                            h a b = isFalse n
                                            @[deprecated]
                                            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)] :
                                            @[deprecated]
                                            theorem imp_of_if_pos {c : Prop} {t : Prop} {e : Prop} [Decidable c] (h : if c then t else e) (hc : c) :
                                            t
                                            @[deprecated]
                                            theorem imp_of_if_neg {c : Prop} {t : Prop} {e : Prop} [Decidable c] (h : if c then t else e) (hnc : ¬c) :
                                            e
                                            @[deprecated]
                                            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
                                            @[deprecated]
                                            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
                                            @[deprecated]
                                            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
                                            @[deprecated]
                                            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
                                            @[deprecated]
                                            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
                                            @[deprecated]
                                            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
                                            @[deprecated]
                                            def AsTrue (c : Prop) [Decidable c] :
                                            Equations
                                            Instances For
                                              @[deprecated]
                                              def AsFalse (c : Prop) [Decidable c] :
                                              Equations
                                              Instances For
                                                @[deprecated]
                                                theorem AsTrue.get {c : Prop} [h₁ : Decidable c] :
                                                AsTrue cc
                                                @[deprecated]
                                                theorem let_value_eq {α : Sort u} {β : Sort v} {a₁ : α} {a₂ : α} (b : αβ) (h : a₁ = a₂) :
                                                (let x := a₁; b x) = let x := a₂; b x
                                                @[deprecated]
                                                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)
                                                @[deprecated]
                                                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
                                                @[deprecated]
                                                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