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.

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

theorem cast_proof_irrel {α : Sort u} {β : Sort u} (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} {φ : α → Sort v} {a : α} {a' : α} {p₁ : φ a} {p₂ : φ a'} (e : a = a') (h₂ : e ▸ p₁ = p₂) : HEq p₁ p₂

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₂

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

Equations

• Xor' a b = (a ∧ ¬b ∨ b ∧ ¬a)

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

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

Equations

• ExistsUnique p = ∃ (x : α), p x ∧ ∀ (y : α), p y → y = x

def Mathlib.Notation.isExplicitBinderSingular (xs : Lean.TSyntax `Lean.explicitBinders) : Bool

Checks to see that xs has only one binder.

Equations

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

def Mathlib.Notation.«term∃!_,_» : Lean.ParserDescr

∃! 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.

def Mathlib.Notation.unexpandExistsUnique : Lean.PrettyPrinter.Unexpander

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.

def Mathlib.Notation.«term∃!__,_» : Lean.ParserDescr

∃! 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.

theorem ExistsUnique.intro {α : Sort u} {p : α → Prop} (w : α) (h₁ : p w) (h₂ : ∀ (y : α), p y → y = w) : ∃! x : α, p x

theorem ExistsUnique.elim {α : Sort u} {p : α → Prop} {b : Prop} (h₂ : ∃! x : α, p x) (h₁ : ∀ (x : α), p x → (∀ (y : α), p y → y = 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} {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} {p : α → Prop} {q : α → Prop} (h : ∀ (a : α), p a ↔ q a) : (∃! a : α, p a) ↔ ∃! a : α, q a

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

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

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₄

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₄

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

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.

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

Alias of instDecidableOr.

Equations

• @Or.decidable = @instDecidableOr

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

Alias of instDecidableAnd.

Equations

• @And.decidable = @instDecidableAnd

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

Alias of instDecidableNot.

Equations

• @Not.decidable = @instDecidableNot

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

Alias of instDecidableIff.

Equations

• @Iff.decidable = @instDecidableIff

def decidableTrue : Decidable True

Alias of instDecidableTrue.

Equations

• decidableTrue = instDecidableTrue

def decidableFalse : Decidable False

Alias of instDecidableFalse.

Equations

• decidableFalse = instDecidableFalse

instance instDecidableXor' (p : Prop) {q : Prop} [Decidable p] [Decidable q] : Decidable (Xor' p q)

Equations

• instDecidableXor' p = inferInstanceAs (Decidable (p ∧ ¬q ∨ q ∧ ¬p))

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

Equations

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

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

Equations

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

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 = match x✝, x with | x, y => if hp : p x y = true then isTrue ⋯ else isFalse ⋯

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

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 : c → x = u) (h_e : ¬c → y = 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] : Prop

Equations

• AsTrue c = if c then True else False

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

Equations

• AsFalse c = if c then False else True

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

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

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 LeftIdentity {α : Type u} (f : α → α → α) (one : α) : Prop

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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)

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