mem_iInf_finite — Mathlib

English

For finite ι, a set s is in the infimum iInf f exactly when there exists a Finset t ⊆ ι such that s ∈ ⨅ i ∈ t, f i.

Русский

Для конечного множества индексов ι: s ∈ iInf f тогда и только тогда, когда существует конечный множество t ⊆ ι такое, что s ∈ ⨅ i ∈ t, f i.

LaTeX

$$$ s \in \iInf f \iff \exists t : Finset ι, s \in \iInf i \in t, f i $$$

Lean4

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

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