atTop_basis' — Mathlib

English

The atTop filter has a basis consisting of tails {a ≤ x} with Ici indexing.

Русский

У фильтра atTop имеется базис из хвостов {a ≤ x} с индексированием Ici.

LaTeX

$$$ \\operatorname{atTop.HasBasis} (a \\le \\cdot) \\mathrm{Ici}$$$

Lean4

theorem atTop_basis' (a : α) : atTop.HasBasis (a ≤ ·) Ici :=
  by
  have : Nonempty α := ⟨a⟩
  refine atTop_basis.to_hasBasis (fun b _ ↦ ?_) fun b _ ↦ ⟨b, trivial, Subset.rfl⟩
  obtain ⟨c, hac, hbc⟩ := exists_ge_ge a b
  exact ⟨c, hac, Ici_subset_Ici.2 hbc⟩

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