atTop_basis_Ioi — Mathlib

English

If α has no maximum, then atTop has a basis consisting of open rays Ioi from each a.

Русский

Если у α нет максимума, то у atTop есть базис, состоящий из лучей Ioi от каждого a.

LaTeX

$$$ \\text{NoMaxOrder}(\\alpha) \\Rightarrow \\operatorname{atTop.HasBasis} (\\,) \\mathrm{Ioi}$$$

Lean4

theorem atTop_basis_Ioi [Nonempty α] [NoMaxOrder α] : (@atTop α _).HasBasis (fun _ => True) Ioi :=
  atTop_basis.to_hasBasis (fun a ha => ⟨a, ha, Ioi_subset_Ici_self⟩) fun a ha =>
    (exists_gt a).imp fun _b hb => ⟨ha, Ici_subset_Ioi.2 hb⟩

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