mem_iInf_finite' — Mathlib

English

Equivalent reformulation: membership in iInf f is equivalent to the existence of a finite subfamily whose iInf is used to represent s.

Русский

Эквивалентная формулировка: членство в iInf f эквивалентно существованию конечной подсемьи, для которой рассматривается iInf и представляется s.

LaTeX

$$$ U \in \iInf f \iff \exists t : Finset ι, U \in \iInf (i \in t) (f i) $$$

Lean4

theorem mem_iInf_finite' {f : ι → Filter α} (s) : s ∈ iInf f ↔ ∃ t : Finset (PLift ι), s ∈ ⨅ i ∈ t, f (PLift.down i) :=
  (Set.ext_iff.1 (iInf_sets_eq_finite' f) s).trans mem_iUnion

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