subset_sInter_iff

Mathlib.Data.Set.Lattice

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

English

t ⊆ ⋂S if and only if ∀ t' ∈ S, t ⊆ t'.

Русский

t ⊆ ⋂S тогда и только тогда, когда ∀ t' ∈ S, t ⊆ t'.

LaTeX

$$$ t \subseteq \bigcap S \iff \forall t' \in S, t \subseteq t' $$$

Lean4

@[simp]
theorem subset_sInter_iff {S : Set (Set α)} {t : Set α} : t ⊆ ⋂₀ S ↔ ∀ t' ∈ S, t ⊆ t' :=
  le_sInf_iff

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

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

Разделы

Аффилиация

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