iInf_principal_finite — Mathlib

English

For any finite index set, the infimum of principal filters is the principal of the intersection over all indices.

Русский

Для любого конечного множества индексов инфимуум главных фильтров равен главному фильтру пересечения по всем индексам.

LaTeX

$$$ \forall f : \iota \to Set α, \; \iInf i, \mathrm{principal}(f(i)) = \mathrm{principal}(\bigcap_i f(i)) $$$

Lean4

theorem iInf_principal_finite {ι : Type w} {s : Set ι} (hs : s.Finite) (f : ι → Set α) :
    ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i) := by
  lift s to Finset ι using hs
  exact mod_cast iInf_principal_finset s f

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