small_sInter'

Mathlib.Logic.Small.Set

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

← MathLib Explorer

English

If s is nonempty and every t ∈ s is small, then ⋂₀ s is small.

Русский

Если s непусто и каждая t ∈ s мала, то ⋂₀ s мала.

LaTeX

$$$[\text{Nonempty } s] \; [\forall t \in s, \operatorname{Small}(t)] \Rightarrow \operatorname{Small}(\bigcap s)$$$

Lean4

instance small_sInter' {s : Set (Set α)} [Nonempty s] [∀ t : s, Small.{u} t] : Small.{u} (⋂₀ s) :=
  let ⟨t⟩ : Nonempty s := inferInstance
  small_sInter t.prop

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

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

Разделы

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

Аффилиация

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