small_sInter

Mathlib.Logic.Small.Set

URI: https://scilib.ai/kg/mathlib#small_sInter

English

If t ∈ s and t is small, then ⋂ s is small.

Русский

Если t ∈ s и t мало, тогда ⋂ s мало.

LaTeX

$$$t \in s \Rightarrow \operatorname{Small}(t) \Rightarrow \operatorname{Small}(\bigcap s)$$$

Lean4

theorem small_sInter {s : Set (Set α)} {t : Set α} (ht : t ∈ s) [Small.{u} t] : Small.{u} (⋂₀ s) :=
  Set.sInter_eq_iInter ▸ small_iInter _ ⟨t, ht⟩

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

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

Разделы

Аффилиация

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