stronglyMeasurable_id — Mathlib

English

The identity function id: α → α is strongly measurable under standard second-countable topologies.

Русский

Тождественная функция id: α → α сильно измерима в стандартных топологиях с счетной базой.

LaTeX

$$$\text{StronglyMeasurable}(\mathrm{id})$$$

Lean4

@[fun_prop, measurability]
theorem _root_.stronglyMeasurable_id [TopologicalSpace α] [PseudoMetrizableSpace α] [OpensMeasurableSpace α]
    [SecondCountableTopology α] : StronglyMeasurable (id : α → α) :=
  measurable_id.stronglyMeasurable

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