English
Let f and g be filters on α with realizers F for f and G for g. Then there exists a realizer for the supremum f ⊔ g, constructed from F and G by taking σ × τ as the index set and defining the member function as unions of F-values and G-values respectively.
Русский
Пусть f и g — фильтры на α с реализаторами F для f и G для g. Тогда существует реализатор для верхней границы f ⊔ g, построенный из F и G: индексное множество σ × τ, а множества задаются объединениями соответствующих значений.
LaTeX
$$$\\text{Realizer}(f \\sqcup g) = \\text{Realizer.sup}(F,G)$ where the underlying index set is $\\sigma_f \\times \\sigma_g$ and the realizations are given by $F.F s \\cup G.F t$ on pairs $(s,t)$.$$
Lean4
/-- Construct a realizer for the sup of two filters -/
protected def sup {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 _ _ ↦ union_subset_union (F.F.inf_le_left _ _) (G.F.inf_le_left _ _)
inf_le_right := fun _ _ ↦ union_subset_union (F.F.inf_le_right _ _) (G.F.inf_le_right _ _) },
filter_eq <| Set.ext fun _ ↦ by cases F; cases G; substs f g; simp [CFilter.toFilter]⟩
