disjointed_add_one — Mathlib

English

If NoMaxOrder holds, then disjointed f (i+1) = f(i+1) \ f i.

Русский

При условии NoMaxOrder выполняется disjointed f (i+1) = f(i+1) \ f i.

LaTeX

$$$ [NoMaxOrder ι] \; \forall f,\; \text{disjointed } f (i+1) = f(i+1) \setminus f(i) $$$

Lean4

protected theorem disjointed_add_one [NoMaxOrder ι] {f : ι → α} (hf : Monotone f) (i : ι) :
    disjointed f (i + 1) = f (i + 1) \ f i :=
  by
  rw [← succ_eq_add_one, hf.disjointed_succ]
  exact not_isMax i

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