isCobounded_sInter

Mathlib.Topology.Bornology.Basic

URI: https://scilib.ai/kg/mathlib#Bornology.isCobounded_sInter

English

For a finite S of sets, the sInter is cobounded iff every member set is cobounded.

Русский

Для конечного S: IsCobounded(S.sInter) эквивалентно ∀ s ∈ S, IsCobounded(s).

LaTeX

$$$\text{IsCobounded}(\bigcap S) \iff \forall s \in S, \text{IsCobounded}(s)$$$

Lean4

theorem isCobounded_sInter {S : Set (Set α)} (hs : S.Finite) : IsCobounded (⋂₀ S) ↔ ∀ s ∈ S, IsCobounded s :=
  sInter_mem hs

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

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

Разделы

Аффилиация

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