iUnion_mono'

Mathlib.Data.Set.Lattice

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

English

If for every i there exists j with s_i ⊆ t_j, then ⋃_i s_i ⊆ ⋃_j t_j.

Русский

Если для каждого i существует j, при котором s_i ⊆ t_j, то ⋃_i s_i ⊆ ⋃_j t_j.

LaTeX

$$$\forall i,\ exists j,\ s_i \subseteq t_j \Rightarrow \bigcup_i s_i \subseteq \bigcup_j t_j$$$

Lean4

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

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

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

Разделы

Аффилиация

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