absorbs_sInter

Mathlib.Topology.Bornology.Absorbs

URI: https://scilib.ai/kg/mathlib#Set.Finite.absorbs_sInter

English

If S is finite, Absorbs G0 (⋂ S) t is equivalent to Absorbs G0 s t for all s in S.

Русский

Если S конечно, Absorbs G0 (∩ S) t эквивалентно Absorbs G0 s t для каждого s∈S.

LaTeX

$$$(hS : S.Finite) : Absorbs G_0 (\bigcap S) t \iff \forall s \in S, Absorbs G_0 s t$$$

Lean4

theorem absorbs_sInter (hS : S.Finite) : Absorbs G₀ (⋂₀ S) t ↔ ∀ s ∈ S, Absorbs G₀ s t :=
  sInter_mem (f := absorbing G₀ t) hS

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

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

Разделы

Аффилиация

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