join_le — Mathlib

English

If f is a filter on filters (f : Filter (Filter α)) and l is a filter on α, and every m in f satisfies m ≤ l, then join f ≤ l.

Русский

Если f — фильтр над фильтрами и l — фильтр на α, и для всех m в f выполняется m ≤ l, то join f ≤ l.

LaTeX

$$$$ \\text{join}(f) \\leq l \\quad\\text{whenever}\\quad \\forall^\\infty m \\in f,\\ m \\le l. $$$$

Lean4

theorem join_le {f : Filter (Filter α)} {l : Filter α} (h : ∀ᶠ m in f, m ≤ l) : join f ≤ l := fun _ hs =>
  h.mono fun _ hm => hm hs

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