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.

(Jeremy Tan: The only non-deprecated thing in this file now is IsSymmOp)

Unbundled algebra classes

These classes were part of an incomplete refactor described here on the github Wiki. However a subset of them are widely used in mathlib3, and it has been tricky to clean this up as this file was in core Lean 3.

class IsSymmOp (α : Sort u) (β : Sort v) (op : α → α → β) : Prop

IsSymmOp α β op where op : α → α → β is the natural generalisation of Std.IsCommutative (β = α) and IsSymm (β = Prop).

• symm_op : ∀ (a b : α), op a b = op b a

theorem IsSymmOp.symm_op {α : Sort u} {β : Sort v} {op : α → α → β} [self : IsSymmOp α β op] (a : α) (b : α) : op a b = op b a

@[instance 100]

instance isSymmOp_of_isCommutative (α : Sort u) (op : α → α → α) [Std.Commutative op] : IsSymmOp α α op

Equations

• ⋯ = ⋯

@[instance 100]

instance isSymmOp_of_isSymm (α : Sort u) (op : α → α → Prop) [IsSymm α op] : IsSymmOp α Prop op

Equations

• ⋯ = ⋯

@[deprecated]

class IsLeftCancel (α : Sort u) (op : α → α → α) : Prop

• left_cancel : ∀ (a b c : α), op a b = op a c → b = c

theorem IsLeftCancel.left_cancel {α : Sort u} {op : α → α → α} [self : IsLeftCancel α op] (a : α) (b : α) (c : α) : op a b = op a c → b = c

@[deprecated]

class IsRightCancel (α : Sort u) (op : α → α → α) : Prop

• right_cancel : ∀ (a b c : α), op a b = op c b → a = c

theorem IsRightCancel.right_cancel {α : Sort u} {op : α → α → α} [self : IsRightCancel α op] (a : α) (b : α) (c : α) : op a b = op c b → a = c

@[deprecated]

class IsTotalPreorder (α : Sort u) (r : α → α → Prop) extends IsTrans , IsTotal : Prop

IsTotalPreorder X r means that the binary relation r on X is total and a preorder.

@[instance 100]

instance isTotalPreorder_isPreorder (α : Sort u) (r : α → α → Prop) [s : IsTotalPreorder α r] : IsPreorder α r

Every total pre-order is a pre-order.

Equations

• ⋯ = ⋯

@[deprecated]

class IsIncompTrans (α : Sort u) (lt : α → α → Prop) : Prop

IsIncompTrans X lt means that for lt a binary relation on X, the incomparable relation fun a b => ¬ lt a b ∧ ¬ lt b a is transitive.

• incomp_trans : ∀ (a b c : α), ¬lt a b ∧ ¬lt b a → ¬lt b c ∧ ¬lt c b → ¬lt a c ∧ ¬lt c a

theorem IsIncompTrans.incomp_trans {α : Sort u} {lt : α → α → Prop} [self : IsIncompTrans α lt] (a : α) (b : α) (c : α) : ¬lt a b ∧ ¬lt b a → ¬lt b c ∧ ¬lt c b → ¬lt a c ∧ ¬lt c a

@[deprecated, instance 100]

instance instIsIncompTransOfIsStrictWeakOrder (α : Sort u) (lt : α → α → Prop) [IsStrictWeakOrder α lt] : IsIncompTrans α lt

Equations

• ⋯ = ⋯

@[deprecated]

theorem incomp_trans {α : Sort u} {r : α → α → Prop} [IsIncompTrans α r] {a : α} {b : α} {c : α} : ¬r a b ∧ ¬r b a → ¬r b c ∧ ¬r c b → ¬r a c ∧ ¬r c a

@[elab_without_expected_type, deprecated]

theorem incomp_trans_of {α : Sort u} (r : α → α → Prop) [IsIncompTrans α r] {a : α} {b : α} {c : α} : ¬r a b ∧ ¬r b a → ¬r b c ∧ ¬r c b → ¬r a c ∧ ¬r c a

@[deprecated]

def StrictWeakOrder.Equiv {α : Sort u} {r : α → α → Prop} (a : α) (b : α) : Prop

Equations

• StrictWeakOrder.Equiv a b = (¬r a b ∧ ¬r b a)

@[deprecated]

theorem StrictWeakOrder.esymm {α : Sort u} {r : α → α → Prop} {a : α} {b : α} : StrictWeakOrder.Equiv a b → StrictWeakOrder.Equiv b a

@[deprecated]

theorem StrictWeakOrder.not_lt_of_equiv {α : Sort u} {r : α → α → Prop} {a : α} {b : α} : StrictWeakOrder.Equiv a b → ¬r a b

@[deprecated]

theorem StrictWeakOrder.not_lt_of_equiv' {α : Sort u} {r : α → α → Prop} {a : α} {b : α} : StrictWeakOrder.Equiv a b → ¬r b a

@[deprecated]

theorem StrictWeakOrder.erefl {α : Sort u} {r : α → α → Prop} [IsStrictWeakOrder α r] (a : α) : StrictWeakOrder.Equiv a a

@[deprecated]

theorem StrictWeakOrder.etrans {α : Sort u} {r : α → α → Prop} [IsStrictWeakOrder α r] {a : α} {b : α} {c : α} : StrictWeakOrder.Equiv a b → StrictWeakOrder.Equiv b c → StrictWeakOrder.Equiv a c

@[deprecated]

instance StrictWeakOrder.isEquiv {α : Sort u} {r : α → α → Prop} [IsStrictWeakOrder α r] : IsEquiv α StrictWeakOrder.Equiv

Equations

• ⋯ = ⋯

def StrictWeakOrder.«term_≈[_]_» : Lean.TrailingParserDescr

The equivalence relation induced by lt

Equations

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

@[deprecated]

theorem isStrictWeakOrder_of_isTotalPreorder {α : Sort u} {le : α → α → Prop} {lt : α → α → Prop} [DecidableRel le] [IsTotalPreorder α le] (h : ∀ (a b : α), lt a b ↔ ¬le b a) : IsStrictWeakOrder α lt

@[deprecated]

instance instIsTotalPreorderLe {α : Type u_1} [LinearOrder α] : IsTotalPreorder α fun (x1 x2 : α) => x1 ≤ x2

Equations

• ⋯ = ⋯

@[deprecated]

instance isStrictWeakOrder_of_linearOrder {α : Type u_1} [LinearOrder α] : IsStrictWeakOrder α fun (x1 x2 : α) => x1 < x2

Equations

• ⋯ = ⋯

@[deprecated]

theorem lt_of_lt_of_incomp {α : Sort u} {lt : α → α → Prop} [IsStrictWeakOrder α lt] [DecidableRel lt] {a : α} {b : α} {c : α} : lt a b → ¬lt b c ∧ ¬lt c b → lt a c

@[deprecated]

theorem lt_of_incomp_of_lt {α : Sort u} {lt : α → α → Prop} [IsStrictWeakOrder α lt] [DecidableRel lt] {a : α} {b : α} {c : α} : ¬lt a b ∧ ¬lt b a → lt b c → lt a c

@[deprecated]

theorem eq_of_incomp {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] {a : α} {b : α} : ¬lt a b ∧ ¬lt b a → a = b

@[deprecated]

theorem eq_of_eqv_lt {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] {a : α} {b : α} : StrictWeakOrder.Equiv a b → a = b

@[deprecated]

theorem incomp_iff_eq {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] [IsIrrefl α lt] (a : α) (b : α) : ¬lt a b ∧ ¬lt b a ↔ a = b

@[deprecated]

theorem eqv_lt_iff_eq {α : Sort u} {lt : α → α → Prop} [IsTrichotomous α lt] [IsIrrefl α lt] (a : α) (b : α) : StrictWeakOrder.Equiv a b ↔ a = b