rec_linear — Mathlib

English

If a predicate p is invariant under successor (p(a) ↔ p(succ a)) for all a, then p(a) is equivalent to p(b) for any a,b.

Русский

Если для всех a выполняется p(a) ⇔ p(succ(a)), то для любых a,b имеет место p(a) ⇔ p(b).

LaTeX

$$$ \forall a,b,\ p(a) \iff p(b) \quad\text{given}\quad \forall x,\ p(x) \iff p(\operatorname{succ}x). $$$

Lean4

theorem rec_linear {p : α → Prop} (hsucc : ∀ a, p a ↔ p (succ a)) (a b : α) : p a ↔ p b :=
  (le_total a b).elim (Succ.rec_iff hsucc) fun h => (Succ.rec_iff hsucc h).symm

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