atTop_basis_Ioi' — Mathlib

English

If α has no maximum, for any a there exists a basis element of atTop of the form {x ∈ α | a < x} with Ioi.

Русский

Если у α нет максимума, для любого a существует элемент базиса atTop в виде {x ∈ α | a < x} с Ioi.

LaTeX

$$$ \\forall a, \\operatorname{atTop.HasBasis} (a < \\cdot) \\mathrm{Ioi}$$$

Lean4

theorem atTop_basis_Ioi' [NoMaxOrder α] (a : α) : atTop.HasBasis (a < ·) Ioi :=
  by
  have : Nonempty α := ⟨a⟩
  refine atTop_basis_Ioi.to_hasBasis (fun b _ ↦ ?_) fun b _ ↦ ⟨b, trivial, Subset.rfl⟩
  obtain ⟨c, hac, hbc⟩ := exists_ge_ge a b
  obtain ⟨d, hcd⟩ := exists_gt c
  exact ⟨d, hac.trans_lt hcd, Ioi_subset_Ioi (hbc.trans hcd.le)⟩

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