atTop_eq_generate_of_not_bddAbove

English

If α is linearly ordered and s is not bounded above, then atTop equals the generate of Ici'' s.

Русский

Если α линейно упорядочено и s не ограничено сверху, тогда atTop равен generate(Ici'' s).

LaTeX

$$$\\text{If } \\mathrm{Not}\\,(\\mathrm{BddAbove}\\ s),\\ (atTop) = \\mathrm{generate}(\\mathrm{Ici}'' s).$$$

Lean4

theorem atTop_eq_generate_of_not_bddAbove [LinearOrder α] {s : Set α} (hs : ¬BddAbove s) :
    (atTop : Filter α) = generate (Ici '' s) :=
  by
  refine atTop_eq_generate_of_forall_exists_le fun x ↦ ?_
  obtain ⟨y, hy, hy'⟩ := not_bddAbove_iff.mp hs x
  exact ⟨y, hy, hy'.le⟩

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