of_isEmpty — Mathlib

English

If the target space β is empty, any map f: α → β is measure-preserving between any measures μa, μb.

Русский

Если цель пустое множество, любое отображение f: α → β сохраняет меру между любыми μa, μb.

LaTeX

$$$[IsEmpty β] \\Rightarrow \\forall f, Measurable f, MeasurePreserving f μa μb$$$

Lean4

@[nontriviality]
theorem of_isEmpty [IsEmpty β] (f : α → β) (μa : Measure α) (μb : Measure β) : MeasurePreserving f μa μb :=
  ⟨measurable_of_subsingleton_codomain _, Subsingleton.elim _ _⟩

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