iSup_eq_iUnion

Mathlib.Order.SetNotation

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

English

For a family of sets s, the indexed supremum equals the indexed union.

Русский

Для семейства множеств s \, iSup равен iUnion.

LaTeX

$$$\mathrm{iSup}\ s = \mathrm{iUnion}\ s$$$

Lean4

@[simp]
theorem iSup_eq_iUnion (s : ι → Set α) : iSup s = iUnion s :=
  rfl

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

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

Разделы

Аффилиация

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