succ_eq_csInf — Mathlib

English

In a Conditionally Complete Lattice with a successor and no maximum, succ(a) equals the csInf of all elements strictly greater than a: succ(a) = sInf(Ioi(a)).

Русский

В условно полную решётку с предшественником и отсутствием максимума, succ(a) = sInf( Ioi(a) ).

LaTeX

$$$ \operatorname{succ} a = \operatorname{sInf}( \{ b \in \alpha \mid a < b \} ) $$$

Lean4

theorem succ_eq_csInf [ConditionallyCompleteLattice α] [SuccOrder α] [NoMaxOrder α] (a : α) :
    succ a = sInf (Set.Ioi a) :=
  by
  apply (le_csInf nonempty_Ioi fun b => succ_le_of_lt).antisymm
  exact csInf_le ⟨a, fun b => le_of_lt⟩ <| lt_succ a

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