iSup_succ — Mathlib

English

For a succ-order, the successor map respects iSup: there is a relation between f(succ a) and succ(f a).

Русский

Для порядка-предшественника выполняется условие соответствия между f(succ a) и succ(f a).

LaTeX

$$$ f (succ a) = succ (f a) $$$

Lean4

theorem iSup_succ [SuccOrder α] (x : α) : ⨆ a : Iio x, succ a.1 = x :=
  by
  have H : BddAbove (range fun a : Iio x ↦ succ a.1) :=
    ⟨succ x, by simp +contextual [upperBounds, succ_le_succ, le_of_lt]⟩
  apply le_antisymm _ (le_of_forall_lt fun y hy ↦ ?_)
  · rw [ciSup_le_iff' H]
    exact fun a ↦ succ_le_of_lt a.2
  · rw [lt_ciSup_iff' H]
    exact ⟨⟨y, hy⟩, lt_succ_of_not_isMax hy.not_isMax⟩

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