hasBasis_top — Mathlib

English

The top filter on any set α has a basis consisting of the whole space, i.e., there is a basis with index a single element and basic set equal to the universal set.

Русский

На множествах α максимальный фильтр имеет базис, состоящий из единого элемента индекса и базисного множества равного всеобщему множеству.

LaTeX

$$$\\big(\\top_{\\mathcal{F}}\\big).HasBasis(\\lambda _ : Unit \\mapsto True)(\\lambda _ : \\mathrm{univ})$$$

Lean4

theorem hasBasis_top : (⊤ : Filter α).HasBasis (fun _ : Unit ↦ True) (fun _ ↦ Set.univ) :=
  ⟨fun U => by simp⟩

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