basis_sets — Mathlib

English

Every filter l has a basis given by its own members: l has basis {s ∈ l} with id as index.

Русский

Каждый фильтр имеет базис, состоящий из собственных подмножеств: l имеет базис {s ∈ l} с единицей в качестве индекса.

LaTeX

$$$l\text{ hasBasis }(s\mapsto s\in l)\;id$$$

Lean4

theorem basis_sets (l : Filter α) : l.HasBasis (fun s : Set α => s ∈ l) id :=
  ⟨fun _ => exists_mem_subset_iff.symm⟩

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