quotientMeasureEqMeasurePreimage_of_zero

English

If a fundamental domain s has ν-measure zero, then the zero measure on the quotient satisfies QuotientMeasureEqMeasurePreimage with respect to ν.

Русский

Если ν-мере ноль на фундаментальной области s, то нулевая мера на факторпространстве удовлетворяет QuotientMeasureEqMeasurePreimage относительно ν.

LaTeX

$$$IsFundamentalDomain(G,s,ν) \\land ν(s) = 0 \\Rightarrow QuotientMeasureEqMeasurePreimage(ν,0).$$$

Lean4

/-- If a fundamental domain has volume 0, then `QuotientMeasureEqMeasurePreimage` holds. -/
@[to_additive]
theorem quotientMeasureEqMeasurePreimage_of_zero {s : Set α} (fund_dom_s : IsFundamentalDomain G s ν)
    (vol_s : ν s = 0) : QuotientMeasureEqMeasurePreimage ν (0 : Measure (Quotient α_mod_G)) :=
  by
  apply fund_dom_s.quotientMeasureEqMeasurePreimage
  ext U meas_U
  simp only [Measure.coe_zero, Pi.zero_apply]
  convert (measure_inter_null_of_null_right (h := vol_s) (Quotient.mk α_mod_G ⁻¹' U)).symm
  rw [measure_map_restrict_apply (meas_U := meas_U)]

Похожие утверждения