hasFundamentalDomain — Mathlib

English

If fund_dom_s and fund_dom_t are fundamental domains for ν, then the induced quotient measures are equal: map( Quotient.mk (orbitRel G α) ) (μ.restrict s) = map( Quotient.mk (orbitRel G α) ) (μ.restrict t).

Русский

Если fund_dom_s и fund_dom_t являются фундаментальными областями относительно ν, то индукированные меры на факторпространстве совпадают: map(Quotient.mk(orbitRel G α))(μ|s) = map(Quotient.mk(orbitRel G α))(μ|t).

LaTeX

$$(μ.restrict s).map (Quotient.mk (MulAction.orbitRel G α)) = (μ.restrict t).map (Quotient.mk (MulAction.orbitRel G α))$$

Lean4

/-- If there is a fundamental domain `s`, then `HasFundamentalDomain` holds. -/
@[to_additive]
theorem hasFundamentalDomain (ν : Measure α) {s : Set α} (fund_dom_s : IsFundamentalDomain G s ν) :
    HasFundamentalDomain G α ν :=
  ⟨⟨s, fund_dom_s⟩⟩

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