isAddFundamentalDomain' — Mathlib

English

A variant of IsAddFundamentalDomain for AddSubgroup holds, replacing spanℤ with the AddSubgroup version.

Русский

Вариант IsAddFundamentalDomain для AddSubgroup сохраняется, заменяя spanℤ на версию AddSubgroup.

LaTeX

$$$\text{IsAddFundamentalDomain}'(\operatorname{span}_{\mathbb{Z}}(\operatorname{range} b)).toAddSubgroup, \operatorname{fundamentalDomain}(b).$$$

Lean4

/-- A version of `ZSpan.isAddFundamentalDomain` for `AddSubgroup`. -/
protected theorem isAddFundamentalDomain' [Finite ι] [MeasurableSpace E] [OpensMeasurableSpace E] (μ : Measure E) :
    IsAddFundamentalDomain (span ℤ (Set.range b)).toAddSubgroup (fundamentalDomain b) μ :=
  ZSpan.isAddFundamentalDomain b μ

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