English
There is a measurable equivalence between Euclidean space and the coordinate function space that identifies points with their coordinates.
Русский
Существует измеримая эквиваленция между Евклидовым пространством и пространством координат, идентифицирующая точку с её координатами.
LaTeX
$$$\text{EuclideanSpace.measurableEquiv}: \mathbb{R}^{\iota} \simeq_m (\iota \to \mathbb{R})$$$
Lean4
/-- If a measure `μ` is left-invariant and satisfies the right scaling condition, then it
satisfies `QuotientMeasureEqMeasurePreimage`. -/
@[to_additive /-- If a measure `μ` is
left-invariant and satisfies the right scaling condition, then it satisfies
`AddQuotientMeasureEqMeasurePreimage`. -/
]
theorem leftInvariantIsQuotientMeasureEqMeasurePreimage [IsFiniteMeasure μ] [hasFun : HasFundamentalDomain Γ.op G ν]
(h : covolume Γ.op G ν = μ univ) : QuotientMeasureEqMeasurePreimage ν μ :=
by
obtain ⟨s, fund_dom_s⟩ := hasFun.ExistsIsFundamentalDomain
have finiteCovol : μ univ < ⊤ := measure_lt_top μ univ
rw [fund_dom_s.covolume_eq_volume] at h
by_cases meas_s_ne_zero : ν s = 0
· convert fund_dom_s.quotientMeasureEqMeasurePreimage_of_zero meas_s_ne_zero
rw [← @measure_univ_eq_zero, ← h, meas_s_ne_zero]
apply
IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set (fund_dom_s := fund_dom_s) (meas_V := MeasurableSet.univ)
· rw [← h]
exact meas_s_ne_zero
· rw [← h]
simp
· rw [← h]
convert finiteCovol.ne
