iInf_principal' — Mathlib

English

For a finite index set s ⊆ ι, the infimum over s of principal sets equals the principal set of the intersection over s.

Русский

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

LaTeX

$$$ \forall s : Finset ι, \; \bigwedge_{i\in s} \mathcal{P}(f(i)) = \mathcal{P}(\bigcap_{i\in s} f(i)) $$$

Lean4

/-- A special case of `iInf_principal` that is safe to mark `simp`. -/
@[simp]
theorem iInf_principal' {ι : Type w} [Finite ι] (f : ι → Set α) : ⨅ i, 𝓟 (f i) = 𝓟 (⋂ i, f i) :=
  iInf_principal _

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