principal_add_iff_add_lt_ne_self — Mathlib

English

Principal (· + ·) a is equivalent to the statement that for all b < a and all c < a, b + c ≠ a.

Русский

Принципиал для сложения в ординале a эквивалентен утверждению: для всех b < a и всех c < a выполняется b + c ≠ a.

LaTeX

$$$Principal(\cdot + \cdot, a) \iff \forall b < a, \forall c < a, b + c \neq a.$$$

Lean4

theorem principal_add_iff_add_lt_ne_self : Principal (· + ·) a ↔ ∀ b < a, ∀ c < a, b + c ≠ a :=
  ⟨fun ha _ hb _ hc => (ha hb hc).ne, fun H => by
    by_contra! ha
    rcases exists_lt_add_of_not_principal_add ha with ⟨b, hb, c, hc, rfl⟩
    exact (H b hb c hc).irrefl⟩

Похожие утверждения