Theorems · Theorem · measure theory

MeasureTheory.FiniteMeasure.Topology.IsClosedEmbedding.isEmbedding_map_finiteMeasure

∀ {Ω' : Type u_2} [inst : MeasurableSpace Ω'] [inst_1 : TopologicalSpace Ω'] [inst_2 : BorelSpace Ω'] {Ω : Type u_3}
  [inst_3 : MeasurableSpace Ω] [inst_4 : TopologicalSpace Ω] [inst_5 : BorelSpace Ω] [NormalSpace Ω'] (f : Ω → Ω'),
  Topology.IsClosedEmbedding f → Topology.IsEmbedding fun μ => μ.map f

Defined in

Mathlib.MeasureTheory.Measure.FiniteMeasure

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceBorelSpaceMeasurableSpaceTopologicalSpaceBorelSpaceNormalSpace