Theorems · Theorem · measure theory

MeasureTheory.Measure.AddMonoidHom.continuous_of_measurable

∀ {G : Type u_1} {H : Type u_2} [inst : SeminormedAddCommGroup G] [inst_1 : MeasurableSpace G] [BorelSpace G]
  [LocallyCompactSpace G] [inst_4 : SeminormedAddCommGroup H] [inst_5 : MeasurableSpace H] [OpensMeasurableSpace H]
  [NormedSpace ℝ H] (f : G →+ H), Measurable ⇑f → Continuous ⇑f

A Borel-measurable group hom from a locally compact normed group to a real normed space is continuous.

Defined in

Mathlib.MeasureTheory.Measure.Haar.NormedSpace

Cited by

0 results in Mathlib

Foundations

Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedAddCommGroupMeasurableSpaceBorelSpaceLocallyCompactSpaceSeminormedAddCommGroupMeasurableSpaceOpensMeasurableSpaceNormedSpace