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 iUnion s ⊆ iUnion t.

Русский

Если s_i ⊆ t_i для всех 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

@[gcongr]
theorem iUnion_mono'' {s t : ι → Set α} (h : ∀ i, s i ⊆ t i) : iUnion s ⊆ iUnion t :=
  iSup_mono h

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

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

Разделы

Аффилиация

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