subset_sInter

Mathlib.Data.Set.Lattice

URI: https://scilib.ai/kg/mathlib#Set.subset_sInter

English

If every t' ∈ S satisfies t ⊆ t', then t ⊆ ⋂S.

Русский

Если для каждого t' ∈ S выполняется t ⊆ t', тогда t ⊆ ⋂S.

LaTeX

$$$ (\forall t' : Set α, t' \in S \rightarrow t \subseteq t') \Rightarrow t \subseteq \bigcap S $$$

Lean4

theorem subset_sInter {S : Set (Set α)} {t : Set α} (h : ∀ t' ∈ S, t ⊆ t') : t ⊆ ⋂₀ S :=
  le_sInf h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru