Theorems · Theorem · general topology

MeasureTheory.measurableSet_range_of_continuous_injective

∀ {γ : Type u_3} {β : Type u_4} [inst : TopologicalSpace γ] [PolishSpace γ] [inst_2 : TopologicalSpace β] [T2Space β]
  [inst_4 : MeasurableSpace β] [OpensMeasurableSpace β] {f : γ → β},
  Continuous f → Function.Injective f → MeasurableSet (Set.range f)

The Lusin-Souslin theorem: the range of a continuous injective function defined on a Polish space is Borel-measurable.

Defined in: Mathlib.MeasureTheory.Constructions.Polish.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace PolishSpace TopologicalSpace T2Space MeasurableSpace OpensMeasurableSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites95

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setproof · cited by 53,352
Realproof · cited by 25,697
TopologicalSpacestatement and proof · cited by 24,529
MeasurableSpacestatement and proof · cited by 13,106
Set.Elemproof · cited by 7,166
Set.imageproof · cited by 5,609
nhdsproof · cited by 5,554
Set.preimageproof · cited by 4,946
Set.rangestatement and proof · cited by 4,705
Filter.Tendstoproof · cited by 3,814
LE.le.transproof · cited by 3,151
MeasurableSetstatement and proof · cited by 3,075

Cited by1

Results whose statement or proof uses this declaration.

IsClosed.measurableSet_image_of_continuousOn_injOnproof · cited by 1