English
Let f and g be filters with realizers F and G. There is a realizer for the infimum f ⊓ g, built from F and G by taking σ × τ as the index and defining the member function as intersections F s ∩ G t.
Русский
Пусть f и g — фильтры с реализаторами F и G. Существует реализатор для пересечения f ∩ g, получаемый из F и G: множество индексов σ × τ и функция-элемент типа ∩.
LaTeX
$$$\\text{Realizer}(f \\inf g) = \\text{Realizer.inf}(F,G)$, with underlying set $\\sigma_f \\times \\sigma_g$ and $f(s,t) = F.F s \\cap G.F t$.$$
Lean4
/-- Construct a realizer for the inf of two filters -/
protected def inf {f g : Filter α} (F : f.Realizer) (G : g.Realizer) : (f ⊓ g).Realizer :=
⟨F.σ × G.σ,
{ f := fun ⟨s, t⟩ ↦ F.F s ∩ G.F t
pt := (F.F.pt, G.F.pt)
inf := fun ⟨a, a'⟩ ⟨b, b'⟩ ↦ (F.F.inf a b, G.F.inf a' b')
inf_le_left := fun _ _ ↦ inter_subset_inter (F.F.inf_le_left _ _) (G.F.inf_le_left _ _)
inf_le_right := fun _ _ ↦ inter_subset_inter (F.F.inf_le_right _ _) (G.F.inf_le_right _ _) },
by
cases F; cases G; substs f g; simp only [CFilter.toFilter, Prod.exists]; ext
constructor
· rintro ⟨s, t, h⟩
apply mem_inf_of_inter _ _ h
· use s
· use t
· rintro ⟨_, ⟨a, ha⟩, _, ⟨b, hb⟩, rfl⟩
exact ⟨a, b, inter_subset_inter ha hb⟩⟩
