English
If h is a fundamental domain and f: α ≃ β is an equivalence with quasi-measure-preserving properties, then the image f''s is a fundamental domain for the corresponding action on β w.r.t. ν.
Русский
Если h — фундаментальная область и f: α ≃ β — эквив, сохраняющий меру в определенном смысле, то образ f''s является фундаментальной областью на β относительно ν.
LaTeX
$$$\\text{IsFundamentalDomain}(H, f''s, ν)$$$
Lean4
@[to_additive]
theorem image_of_equiv {ν : Measure β} (h : IsFundamentalDomain G s μ) (f : α ≃ β)
(hf : QuasiMeasurePreserving f.symm ν μ) (e : H ≃ G) (hef : ∀ g, Semiconj f (e g • ·) (g • ·)) :
IsFundamentalDomain H (f '' s) ν := by
rw [f.image_eq_preimage]
refine h.preimage_of_equiv hf e.symm.bijective fun g x => ?_
rcases f.surjective x with ⟨x, rfl⟩
rw [← hef _ _, f.symm_apply_apply, f.symm_apply_apply, e.apply_symm_apply]
