sInter_subset_of_mem

Mathlib.Data.Set.Lattice

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

English

If t ∈ S, then the intersection over S is contained in t.

Русский

Если t ∈ S, то пересечение ⋂S содержится в t.

LaTeX

$$$ t \in S \rightarrow \bigcap S \subseteq t $$$

Lean4

theorem sInter_subset_of_mem {S : Set (Set α)} {t : Set α} (tS : t ∈ S) : ⋂₀ S ⊆ t :=
  sInf_le tS

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

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

Разделы

Аффилиация

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