English
Let e: α → β be a measurable embedding which induces the topology on α. If β is a Borel space, then α is a Borel space.
Русский
Пусть e: α → β будет измеримо вложением, порождающим топологию α. Если β — пространство Бореля, то α — пространство Бореля.
LaTeX
$$$(MeasurableEmbedding\, e) \land (IsInducing\, e) \land BorelSpace\, \beta \\Rightarrow BorelSpace\, \\alpha$$$
Lean4
/-- Given a measurable embedding to a Borel space which is also a topological embedding, then the
source space is also a Borel space. -/
theorem borelSpace {α β : Type*} [MeasurableSpace α] [TopologicalSpace α] [MeasurableSpace β] [TopologicalSpace β]
[hβ : BorelSpace β] {e : α → β} (h'e : MeasurableEmbedding e) (h''e : IsInducing e) : BorelSpace α :=
by
constructor
have : MeasurableSpace.comap e (borel β) = ‹_› := by simpa [hβ.measurable_eq] using h'e.comap_eq
rw [← this, ← borel_comap, h''e.eq_induced]
