fundamentalInterior_subset — Mathlib

English

The interior of the fundamental domain is contained in the domain: fundamentalInterior(G,s) ⊆ s.

Русский

Внутренняя часть фундаментальной области содержится в самой области: fundamentalInterior(G,s) ⊆ s.

LaTeX

$$$\\mathrm{fundamentalInterior}(G,s) \\subseteq s$$$

Lean4

@[to_additive MeasureTheory.addFundamentalInterior_subset]
theorem fundamentalInterior_subset : fundamentalInterior G s ⊆ s :=
  diff_subset

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