comap_id

Mathlib.MeasureTheory.Measure.Comap

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.comap_id

← MathLib Explorer

English

Composing with the identity map preserves the measure: comap id μ = μ.

Русский

Комап идентичности сохраняет меру: comap id μ = μ.

LaTeX

$$$\\mathrm{comap}\\ \\text{id}\\, \\mu = \\mu$$$

Lean4

@[simp]
theorem comap_id (μ : Measure β) : comap (fun x ↦ x) μ = μ :=
  by
  ext s hs
  rw [comap_apply, image_id']
  · exact injective_id
  all_goals simp [*]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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