English
There exists a Polish topology refining the original such that s becomes closed and open simultaneously (clopen).
Русский
Существует топология Полиша, уточняющая исходную, для которой множество становится одновременно замкнутым и открытым.
LaTeX
$$∃ t', Polish t', IsClosed s ∧ IsOpen s$$
Lean4
/-- The image of a measurable set under a monotone map is measurable. -/
theorem image_of_monotoneOn [SecondCountableTopology β] (ht : MeasurableSet t) (hg : MonotoneOn g t) :
MeasurableSet (g '' t) := by
/- Since there are only countably many discontinuity points, the result follows by reduction to
the continuous case, which we have already proved. -/
let t' := {x ∈ t | ¬ContinuousWithinAt g t x}
have ht' : Set.Countable t' := hg.countable_not_continuousWithinAt
have : g '' t = g '' (t \ t') ∪ g '' t' := by
rw [← image_union]
congr!
ext
simp only [sdiff_sep_self, not_not, mem_union, mem_setOf_eq, t']
tauto
rw [this]
apply MeasurableSet.union _ (ht'.image g).measurableSet
apply MeasurableSet.image_of_monotoneOn_of_continuousOn (ht.diff ht'.measurableSet) (hg.mono diff_subset)
intro x hx
simp only [sdiff_sep_self, not_not, mem_setOf_eq, t'] at hx
exact hx.2.mono diff_subset
