apply_of_isSuccLimit — Mathlib

English

If f is normal and a is a succ-limit, then f(a) equals the supremum of f on all b with b < a.

Русский

Если f нормальная и a является succ-пределом, то f(a) равно supremum значений f(b) для всех b < a.

LaTeX

$$$\\mathrm{IsNormal}(f) \\Rightarrow \\mathrm{IsSuccLimit}(a) \\Rightarrow f(a) = \\big(\\bigvee_{b \\in Iio(a)} f(b)\\big).$$$

Lean4

theorem apply_of_isSuccLimit (hf : IsNormal f) (ha : IsSuccLimit a) : f a = ⨆ b : Iio a, f b :=
  by
  convert map_iSup hf _
  · exact ha.iSup_Iio.symm
  · exact ⟨⊥, ha.bot_lt⟩
  · use a
    rintro _ ⟨⟨x, hx⟩, rfl⟩
    exact hx.le

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