hasBasis_principal — Mathlib

English

For any set t, the principal filter has a canonical basis given by the basic subset t, via a singleton-type indexing or equivalently via a unit index with t as the basic set.

Русский

Для любого множества t принципиальный фильтр имеет канонический базис, заданный подмножеством t.

LaTeX

$$$\\text{HasBasis}(\\mathcal{P}(t))(\\lambda _ : Unit \\mapsto True)(\\lambda _ : t)$$$

Lean4

theorem hasBasis_principal (t : Set α) : (𝓟 t).HasBasis (fun _ : Unit => True) fun _ => t :=
  ⟨fun U => by simp⟩

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