measurable_mk' — Mathlib

English

The natural map x ↦ x in Real onto the additive circle AddCircle a is measurable with respect to the standard Borel structure.

Русский

Естественный отображение x ↦ x в рожде AddCircle a измеримо относительно стандартной борелевской структуры.

LaTeX

$$$\\text{Measurable}((\\uparrow): \\mathbb{R} \\to \\mathrm{AddCircle}(a))$$$

Lean4

@[measurability]
protected theorem measurable_mk' {a : ℝ} : Measurable (β := AddCircle a) ((↑) : ℝ → AddCircle a) :=
  Continuous.measurable <| AddCircle.continuous_mk' a

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