hasBasis_pure — Mathlib

English

The pure (Dirac) filter at a point x has a basis consisting of the singleton {x} for a unit-indexed basis.

Русский

Пусть x фиксировано; фильтр на точку x имеет базис, состоящий из множества {x}.

LaTeX

$$$\\text{HasBasis}(\\mathrm{pure}\,x)(\\lambda _ : Unit \\mapsto True)(\\lambda _ : \\{x\\})$$$

Lean4

theorem hasBasis_pure (x : α) : (pure x : Filter α).HasBasis (fun _ : Unit => True) fun _ => { x } := by
  simp only [← principal_singleton, hasBasis_principal]

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