mem_iInf_of_directed — Mathlib

English

If f is directed and nonempty, then s ∈ iInf f iff ∃ i, s ∈ f_i.

Русский

Если f удовлетворяет направленности и непусто, то s ∈ iInf f тогда и только тогда, когда ∃ i, s ∈ f_i.

LaTeX

$$s ∈ iInf f ↔ ∃ i, s ∈ f i$$

Lean4

theorem mem_iInf_of_directed {f : ι → Filter α} (h : Directed (· ≥ ·) f) [Nonempty ι] (s) : s ∈ iInf f ↔ ∃ i, s ∈ f i :=
  by simp only [← Filter.mem_sets, iInf_sets_eq h, mem_iUnion]

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