eq_biInf_of_mem_iff_exists_mem — Mathlib

English

Let f be a family of filters indexed by i and p a predicate on i. If l ∈ f_i iff ∃ i with p(i) and s ∈ f_i, then l equals the biInf over i with p(i).

Русский

Пусть имеется семейство фильтров f_i и предикат p(i). Если l ∈ f_i эквивалентно ∃ i с p(i) и s ∈ f_i, тогда l = ⨅_{i: p(i)} f_i.

LaTeX

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

Lean4

theorem eq_biInf_of_mem_iff_exists_mem {f : ι → Filter α} {p : ι → Prop} {l : Filter α}
    (h : ∀ {s}, s ∈ l ↔ ∃ i, p i ∧ s ∈ f i) : l = ⨅ (i) (_ : p i), f i :=
  by
  rw [iInf_subtype']
  exact eq_iInf_of_mem_iff_exists_mem fun {_} => by simp only [Subtype.exists, h, exists_prop]

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