stableUnderGeneralization_iInter — Mathlib

English

If each S(i) is stable under generalization, then the intersection across i is stable under generalization.

Русский

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

LaTeX

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

Lean4

theorem stableUnderGeneralization_iInter {ι : Sort*} (S : ι → Set X) (H : ∀ i, StableUnderGeneralization (S i)) :
    StableUnderGeneralization (⋂ i, S i) :=
  isUpperSet_iInter H

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