biInf_sets_eq — Mathlib

English

Let f: ι → Filter α, p(i) a predicate. If ∀ {s}, s ∈ l ↔ ∃ i, p(i) ∧ s ∈ f_i, then l = ⨅ i (p i), f_i.

Русский

Пусть f_i — фильтры и p(i) предикат. Если ∀ {s}, s ∈ l ↔ ∃ i, p(i) ∧ s ∈ f_i, то l = ⨅ i, p(i) . f_i.

LaTeX

$$l = ⨅ (i) (_ : p i), f i$$

Lean4

theorem biInf_sets_eq {f : β → Filter α} {s : Set β} (h : DirectedOn (f ⁻¹'o (· ≥ ·)) s) (ne : s.Nonempty) :
    (⨅ i ∈ s, f i).sets = ⋃ i ∈ s, (f i).sets :=
  ext fun t => by simp [mem_biInf_of_directed h ne]

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