English
For filters f and g with realizers F and G, f ≤ g if and only if for every b in G.σ there exists a in F.σ such that F.F a ≤ G.F b.
Русский
Пусть у фильтров f и g есть реализаторы F и G. Тогда f ≤ g тогда и только тогда, когда для каждого b из G.σ существует a из F.σ такое, что F.F a ≤ G.F b.
LaTeX
$$$f \\le g \\iff \\forall b : G.σ, \\exists a : F.σ, F.F a \\le G.F b$$$
Lean4
theorem le_iff {f g : Filter α} (F : f.Realizer) (G : g.Realizer) : f ≤ g ↔ ∀ b : G.σ, ∃ a : F.σ, F.F a ≤ G.F b :=
⟨fun H t ↦ F.mem_sets.1 (H (G.mem_sets.2 ⟨t, Subset.refl _⟩)), fun H _ h ↦
F.mem_sets.2 <|
let ⟨s, h₁⟩ := G.mem_sets.1 h
let ⟨t, h₂⟩ := H s
⟨t, Subset.trans h₂ h₁⟩⟩
