map_sup

Mathlib.Order.Filter.Map

URI: https://scilib.ai/kg/mathlib#Filter.map_sup

English

The map operation commutes with arbitrary iSup: map m (⨆ i, f i) = ⨆ i, map m (f i).

Русский

Операция map commute c произвольным iSup: map m (⨆ i, f i) = ⨆ i, map m (f i).

LaTeX

$$$\\mathrm{map}\\ m\\ (\\big\\vee_{i} f_i) = \\big\\vee_{i} (\\mathrm{map}\\ m\\ f_i)$$$

Lean4

@[simp]
theorem map_sup : map m (f₁ ⊔ f₂) = map m f₁ ⊔ map m f₂ :=
  (gc_map_comap m).l_sup

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

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

Разделы

Аффилиация

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