succ_eq_iInf — Mathlib

English

In a complete lattice with a successor, succ(a) equals the infimum of all elements strictly greater than a: succ(a) = ⨅{b > a} b.

Русский

В полной решётке с переходом к следующему элементу, succ(a) есть Inf всех элементов больше a: succ(a) = ⨅_{b > a} b.

LaTeX

$$$ \operatorname{succ} a = \inf\{ b > a \} b $$$

Lean4

theorem succ_eq_iInf [CompleteLattice α] [SuccOrder α] (a : α) : succ a = ⨅ b > a, b := by
  rw [succ_eq_sInf, iInf_subtype', iInf, Subtype.range_coe_subtype, Ioi]

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