map_top

Mathlib.MeasureTheory.MeasurableSpace.Basic

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

English

The top measurable structure remains top under mapping.

Русский

Верхняя структура измеримости остаётся верхней после отображения.

LaTeX

$$$$ (\top : \mathrm{MeasurableSpace}\, \alpha).\mathrm{map}\, f = \top $$$$

Lean4

@[simp]
theorem map_top : (⊤ : MeasurableSpace α).map f = ⊤ :=
  (gc_comap_map f).u_top

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

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

Разделы

Аффилиация

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