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.

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

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

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

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

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

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

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

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

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

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

theorem iff_self_iff (a : Prop) : (a ↔ a) ↔ True

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