English
A function f is a measurable embedding iff it is injective, its comap matches the original measurable space, and the range is measurable.
Русский
Функция f является измеримым вложением тогда и только тогда, когда она инъективна, comap совпадает с исходной структурой, и множество образа измеримо.
LaTeX
$$$\\mathrm{MeasurableEmbedding}(f) \\iff (\\mathrm{Injective}(f) \\wedge \\mathrm{MeasurableSpace.comap} f = \\mathrm{MeasurableSpace} \\wedge \\mathrm{MeasurableSet}(\\mathrm{range}(f)))$$$
Lean4
theorem iff_comap_eq :
MeasurableEmbedding f ↔ Injective f ∧ MeasurableSpace.comap f ‹_› = ‹_› ∧ MeasurableSet (range f) :=
⟨fun hf ↦ ⟨hf.injective, hf.comap_eq, hf.measurableSet_range⟩, fun hf ↦
{ injective := hf.1
measurable := by rw [← hf.2.1]; exact comap_measurable f
measurableSet_image' := by
rw [← hf.2.1]
rintro _ ⟨s, hs, rfl⟩
simpa only [image_preimage_eq_inter_range] using hs.inter hf.2.2 }⟩
