Ioi_pred_eq_insert — Mathlib

English

The set of elements strictly greater than pred a equals the union of {a} with the elements strictly greater than a.

Русский

Множество элементов строго больше чем pred a равно объединению {a} с множеством элементов, больших чем a.

LaTeX

$$$ \\mathrm{Ioi}(\\mathrm{pred}\\ a) = \\mathrm{insert}\\ a\\ (\\mathrm{Ioi}\\ a) $$$

Lean4

theorem Ioi_pred_eq_insert (a : α) : Ioi (pred a) = insert a (Ioi a) :=
  ext fun _ => pred_lt_iff_eq_or_lt.trans <| or_congr_left eq_comm

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