sUnion_mem_empty_univ

Mathlib.Data.Set.Lattice

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

← MathLib Explorer

English

If S is a subset of T, then the intersection over T is contained in the intersection over S.

Русский

Если S ⊆ T, то ⋂T ⊆ ⋂S.

LaTeX

$$$ S \subseteq T \rightarrow \bigcap T \subseteq \bigcap S $$$

Lean4

/-- If all sets in a collection are either `∅` or `Set.univ`, then so is their union. -/
theorem sUnion_mem_empty_univ {S : Set (Set α)} (h : S ⊆ {∅, univ}) : ⋃₀ S ∈ ({∅, univ} : Set (Set α)) := by grind

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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