mem_biInf_of_directed — Mathlib

English

For f: β → Filter α and s ⊆ α, (t ∈ ⨅ i ∈ s, f_i) iff ∃ i ∈ s with t ∈ f_i.

Русский

Для семейства фильтров f_i и множества s, t ∈ ⨅ i ∈ s, f_i тогда и только тогда, когда ∃ i ∈ s: t ∈ f_i.

LaTeX

$$(t ∈ ⨅ i ∈ s, f i) ↔ ∃ i ∈ s, t ∈ f i$$

Lean4

theorem mem_biInf_of_directed {f : β → Filter α} {s : Set β} (h : DirectedOn (f ⁻¹'o (· ≥ ·)) s) (ne : s.Nonempty)
    {t : Set α} : (t ∈ ⨅ i ∈ s, f i) ↔ ∃ i ∈ s, t ∈ f i :=
  by
  haveI := ne.to_subtype
  simp_rw [iInf_subtype', mem_iInf_of_directed h.directed_val, Subtype.exists, exists_prop]

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