map_iSup

Mathlib.Order.OrdContinuous

URI: https://scilib.ai/kg/mathlib#LeftOrdContinuous.map_iSup

Lean4

theorem map_iSup (hf : LeftOrdContinuous f) (g : ι → α) : f (⨆ i, g i) = ⨆ i, f (g i) :=
  by
  simp only [iSup, hf.map_sSup', ← range_comp]
  rfl

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

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

Разделы

Аффилиация

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