English
If s is closed, f is continuous on s and injective on s, then the image f''s is measurable.
Русский
Если s замкнуто, f непрерывна и инъективна на s, то образ f''s измерим.
LaTeX
$$MeasurableSet (f '' s)$$
Lean4
theorem image_of_monotoneOn_of_continuousOn (ht : MeasurableSet t) (hg : MonotoneOn g t) (h'g : ContinuousOn g t) :
MeasurableSet (g '' t) := by
/- We use that the image of a measurable set by a continuous injective map is measurable.
Therefore, we need to remove the points where the map is not injective. There are only countably
many points that have several preimages, so this set is also measurable. -/
let u : Set β := {c | ∃ x, ∃ y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
have hu : Set.Countable u := MonotoneOn.countable_setOf_two_preimages hg
let t' := t ∩ g ⁻¹' u
have ht' : MeasurableSet t' :=
by
have : t' = ⋃ c ∈ u, t ∩ g ⁻¹' { c } := by ext; simp [t']
rw [this]
apply MeasurableSet.biUnion hu (fun c hc ↦ ?_)
obtain ⟨v, hv, tv⟩ : ∃ v, OrdConnected v ∧ t ∩ g ⁻¹' { c } = t ∩ v := ordConnected_singleton.preimage_monotoneOn hg
exact tv ▸ ht.inter hv.measurableSet
have : g '' t = g '' (t \ t') ∪ g '' t' := by simp [← image_union, t']
rw [this]
apply MeasurableSet.union
· apply (ht.diff ht').image_of_continuousOn_injOn (h'g.mono diff_subset)
intro x hx y hy hxy
contrapose! hxy
wlog H : x < y generalizing x y with h
· have : y < x := lt_of_le_of_ne (not_lt.1 H) hxy.symm
exact (h hy hx hxy.symm this).symm
intro h
exact hx.2 ⟨hx.1, x, y, hx.1, hy.1, H, rfl, h.symm⟩
· exact hu.mono (by simp [t']) |>.measurableSet
