iUnion

Mathlib.Order.UpperLower.Relative

URI: https://scilib.ai/kg/mathlib#IsRelUpperSet.iUnion

English

IsRelUpperSet.iUnion: union over a family of sets preserves IsRelUpperSet.

Русский

IsRelUpperSet.iUnion: объединение по семейству множеств сохраняет IsRelUpperSet.

LaTeX

$$$(∀ i, IsRelUpperSet (f i) P) \\Rightarrow IsRelUpperSet (\\bigcup_i f(i)) P$$$

Lean4

protected theorem iUnion {f : ι → Set α} (hf : ∀ i, IsRelUpperSet (f i) P) : IsRelUpperSet (⋃ i, f i) P :=
  .sUnion (forall_mem_range.2 hf)

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

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

Разделы

Аффилиация

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