English
The Realizer ofFilter provides a canonical Realizer for any Filter by taking its sets as the base and the inclusions as the infimum structure.
Русский
Реализатор ofFilter задаёт канонический реализатор для любого фильтра, используя множества фильтра как основание и включения как инфимум-структуру.
LaTeX
$$$\\mathrm{Realizer.ofFilter}: \\text{Filter }\\alpha \\to (\\text{Filter }\\alpha)\\text{Realizer},\\; f\\mapsto \\langle f.sets,\\dots\\rangle$$$
Lean4
/-- A filter realizes itself. -/
def ofFilter (f : Filter α) : f.Realizer :=
⟨f.sets,
{ f := Subtype.val
pt := ⟨univ, univ_mem⟩
inf := fun ⟨_, h₁⟩ ⟨_, h₂⟩ ↦ ⟨_, inter_mem h₁ h₂⟩
inf_le_left := fun ⟨_, _⟩ ⟨_, _⟩ ↦ inter_subset_left
inf_le_right := fun ⟨_, _⟩ ⟨_, _⟩ ↦ inter_subset_right },
filter_eq <| Set.ext fun _ ↦ by simp [exists_mem_subset_iff]⟩
