comap_iSup

Mathlib.MeasureTheory.MeasurableSpace.Basic

URI: https://scilib.ai/kg/mathlib#MeasurableSpace.comap_iSup

English

Pullback commutes with arbitrary suprema: comap g distributes over iSup.

Русский

Обратное отображение комапа коммутирует с произвольной верхней сверткой (iSup).

LaTeX

$$$$ (\bigsqcup_i m_i).\mathrm{comap}\, g = \bigsqcup_i (m_i.\mathrm{comap}\, g) $$$$

Lean4

@[simp]
theorem comap_iSup {m : ι → MeasurableSpace α} : (⨆ i, m i).comap g = ⨆ i, (m i).comap g :=
  (gc_comap_map g).l_iSup

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

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

Разделы

Аффилиация

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