stableUnderSpecialization_iInter — Mathlib

English

If each S(i) is stable under specialization, then the intersection over i is stable under specialization.

Русский

Если каждый S(i) устойчив по специализации, то пересечение по i стабильно по специализации.

LaTeX

$$$\forall i, StableUnderSpecialization(S(i)) \Rightarrow StableUnderSpecialization(\bigcap_i S(i))$$$

Lean4

theorem stableUnderSpecialization_iInter {ι : Sort*} (S : ι → Set X) (H : ∀ i, StableUnderSpecialization (S i)) :
    StableUnderSpecialization (⋂ i, S i) :=
  isLowerSet_iInter H

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