iUnion_mono

Mathlib.Data.Set.Lattice

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

English

If s_i ⊆ t_i for all i, then ⋃_i s_i ⊆ ⋃_i t_i.

Русский

Если для каждого i верно s_i ⊆ t_i, то ⋃_i s_i ⊆ ⋃_i t_i.

LaTeX

$$$\forall i,\ s_i \subseteq t_i \Rightarrow \bigcup_i s_i \subseteq \bigcup_i t_i$$$

Lean4

theorem iUnion_mono {s t : ι → Set α} (h : ∀ i, s i ⊆ t i) : ⋃ i, s i ⊆ ⋃ i, t i :=
  iSup_mono h

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

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

Разделы

Аффилиация

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