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 of_eq_false]

theorem not_of_eq_false {p : Prop} (h : p = False) : ¬p

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₂ : e ▸ p₁ = 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₁ = e ▸ p₂) : 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) : p ∧ True ↔ p

@[deprecated true_and]

theorem true_and_iff (p : Prop) : True ∧ p ↔ p

@[deprecated and_false]

theorem and_false_iff (p : Prop) : p ∧ False ↔ False

@[deprecated false_and]

theorem false_and_iff (p : Prop) : False ∧ p ↔ False

@[deprecated or_true]

theorem or_true_iff (p : Prop) : p ∨ True ↔ True

@[deprecated true_or]

theorem true_or_iff (p : Prop) : True ∨ p ↔ True

@[deprecated or_false]

theorem or_false_iff (p : Prop) : p ∨ False ↔ p

@[deprecated false_or]

theorem false_or_iff (p : Prop) : False ∨ p ↔ p

@[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} : (a ↔ False) ↔ ¬a

@[deprecated false_iff]

theorem false_iff_iff {a : Prop} : (False ↔ a) ↔ ¬a

@[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]

theorem decide_True' (h : Decidable True) : decide True = true

@[deprecated]

theorem decide_False' (h : Decidable False) : decide False = false

@[deprecated]

def Decidable.recOn_true (p : Prop) [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : p) (h₄ : h₁ h₃) : Decidable.recOn h h₂ h₁

Equations

• Decidable.recOn_true p h₃ h₄ = cast ⋯ h₄

@[deprecated]

def Decidable.recOn_false (p : Prop) [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : ¬p) (h₄ : h₂ h₃) : Decidable.recOn h h₂ h₁

Equations

• Decidable.recOn_false p h₃ h₄ = cast ⋯ h₄

@[deprecated Decidable.byCases]

def Decidable.by_cases {p : Prop} {q : Sort u} [dec : Decidable p] (h1 : p → q) (h2 : ¬p → q) : 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

• @Decidable.by_cases = @Decidable.byCases

@[deprecated Decidable.byContradiction]

theorem Decidable.by_contradiction {p : Prop} [dec : Decidable p] (h : ¬p → False) : p

Alias of Decidable.byContradiction.

@[deprecated Decidable.not_not]

theorem Decidable.not_not_iff {p : Prop} [Decidable p] : ¬¬p ↔ p

Alias of Decidable.not_not.

@[deprecated instDecidableOr]

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

Alias of instDecidableOr.

Equations

• @Or.decidable = @instDecidableOr

@[deprecated instDecidableAnd]

def And.decidable {p : Prop} {q : Prop} [dp : Decidable p] [dq : Decidable q] : Decidable (p ∧ q)

Alias of instDecidableAnd.

Equations

• @And.decidable = @instDecidableAnd

@[deprecated instDecidableNot]

def Not.decidable {p : Prop} [dp : Decidable p] : Decidable ¬p

Alias of instDecidableNot.

Equations

• @Not.decidable = @instDecidableNot

@[deprecated instDecidableIff]

def Iff.decidable {p : Prop} {q : Prop} [Decidable p] [Decidable q] : Decidable (p ↔ q)

Alias of instDecidableIff.

Equations

• @Iff.decidable = @instDecidableIff

@[deprecated instDecidableTrue]

def decidableTrue : Decidable True

Alias of instDecidableTrue.

Equations

• decidableTrue = instDecidableTrue

@[deprecated instDecidableFalse]

def decidableFalse : Decidable False

Alias of instDecidableFalse.

Equations

• decidableFalse = instDecidableFalse

@[deprecated]

def IsDecEq {α : Sort u} (p : α → α → Bool) : Prop

Equations

• IsDecEq p = ∀ ⦃x y : α⦄, p x y = true → x = y

@[deprecated]

def IsDecRefl {α : Sort u} (p : α → α → Bool) : Prop

Equations

• IsDecRefl p = ∀ (x : α), p x x = true

@[deprecated]

def decidableEq_of_bool_pred {α : Sort u} {p : α → α → Bool} (h₁ : IsDecEq p) (h₂ : IsDecRefl p) : DecidableEq α

Equations

• decidableEq_of_bool_pred h₁ h₂ x✝ x = if hp : p x✝ x = true then isTrue ⋯ else isFalse ⋯

@[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₁ : p → Sort u} {h₂ : ¬p → Sort u} [h₃ : ∀ (h : p), Subsingleton (h₁ h)] [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)] : Subsingleton (Decidable.recOn h 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] : Prop

Equations

• AsTrue c = if c then True else False

@[deprecated]

def AsFalse (c : Prop) [Decidable c] : Prop

Equations

• AsFalse c = if c then False else True

@[deprecated]

theorem AsTrue.get {c : Prop} [h₁ : Decidable c] : AsTrue c → c

@[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

def Reflexive {β : Sort v} (r : β → β → Prop) : Prop

A reflexive relation relates every element to itself.

Equations

• Reflexive r = ∀ (x : β), r x x

def Symmetric {β : Sort v} (r : β → β → Prop) : Prop

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

Equations

• Symmetric r = ∀ ⦃x y : β⦄, r x y → r y x

def Transitive {β : Sort v} (r : β → β → Prop) : Prop

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

Equations

• Transitive r = ∀ ⦃x y z : β⦄, r x y → r y z → r x z

theorem Equivalence.reflexive {β : Sort v} {r : β → β → Prop} (h : Equivalence r) : Reflexive r

theorem Equivalence.symmetric {β : Sort v} {r : β → β → Prop} (h : Equivalence r) : Symmetric r

theorem Equivalence.transitive {β : Sort v} {r : β → β → Prop} (h : Equivalence r) : Transitive r

def Total {β : Sort v} (r : β → β → Prop) : Prop

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

Equations

• Total r = ∀ (x y : β), r x y ∨ r y x

def Irreflexive {β : Sort v} (r : β → β → Prop) : Prop

Irreflexive means "not reflexive".

Equations

• Irreflexive r = ∀ (x : β), ¬r x x

def AntiSymmetric {β : Sort v} (r : β → β → Prop) : Prop

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

Equations

• AntiSymmetric r = ∀ ⦃x y : β⦄, r x y → r y x → x = y

def EmptyRelation {α : Sort u} : α → α → Prop

An empty relation does not relate any elements.

Equations

• EmptyRelation x✝ x = False

theorem InvImage.trans {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) (h : Transitive r) : Transitive (InvImage r f)

theorem InvImage.irreflexive {α : Sort u} {β : Sort v} (r : β → β → Prop) (f : α → β) (h : Irreflexive r) : Irreflexive (InvImage r f)

@[deprecated]

def LeftIdentity {α : Type u} (f : α → α → α) (one : α) : Prop

Equations

• LeftIdentity f one = ∀ (a : α), f one a = a

@[deprecated]

def RightIdentity {α : Type u} (f : α → α → α) (one : α) : Prop

Equations

• RightIdentity f one = ∀ (a : α), f a one = a

@[deprecated]

def RightInverse {α : Type u} (f : α → α → α) (inv : α → α) (one : α) : Prop

Equations

• RightInverse f inv one = ∀ (a : α), f a (inv a) = one

@[deprecated]

def LeftCancelative {α : Type u} (f : α → α → α) : Prop

Equations

• LeftCancelative f = ∀ (a b c : α), f a b = f a c → b = c

@[deprecated]

def RightCancelative {α : Type u} (f : α → α → α) : Prop

Equations

• RightCancelative f = ∀ (a b c : α), f a b = f c b → a = c

@[deprecated]

def LeftDistributive {α : Type u} (f : α → α → α) (g : α → α → α) : Prop

Equations

• LeftDistributive f g = ∀ (a b c : α), f a (g b c) = g (f a b) (f a c)

@[deprecated]

def RightDistributive {α : Type u} (f : α → α → α) (g : α → α → α) : Prop

Equations

• RightDistributive f g = ∀ (a b c : α), f (g a b) c = g (f a c) (f b c)

def Commutative {α : Type u} (f : α → α → α) : Prop

Equations

• Commutative f = ∀ (a b : α), f a b = f b a

def Associative {α : Type u} (f : α → α → α) : Prop

Equations

• Associative f = ∀ (a b c : α), f (f a b) c = f a (f b c)

def RightCommutative {α : Type u} {β : Type v} (h : β → α → β) : Prop

Equations

• RightCommutative h = ∀ (b : β) (a₁ a₂ : α), h (h b a₁) a₂ = h (h b a₂) a₁

def LeftCommutative {α : Type u} {β : Type v} (h : α → β → β) : Prop

Equations

• LeftCommutative h = ∀ (a₁ a₂ : α) (b : β), h a₁ (h a₂ b) = h a₂ (h a₁ b)

theorem left_comm {α : Type u} (f : α → α → α) : Commutative f → Associative f → LeftCommutative f

theorem right_comm {α : Type u} (f : α → α → α) : Commutative f → Associative f → RightCommutative f