Mathlib Map

Theorems · Definition · measure theory

MeasureTheory.fundamentalInterior

(G : Type u_1) → {α : Type u_3} → [inst : Group G] → [MulAction G α] → Set α → Set α

The interior of a fundamental domain, those points of the domain not lying in any translate.

Defined in
Mathlib.MeasureTheory.Group.FundamentalDomain
Cited by
12 results in Mathlib
Foundations
Depth 12 from the axioms · uses propext
Assumes
GroupMulAction
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MeasureTheory.pairwise_disjoint_fundamentalInterior · cited by 1MeasureTheory.pairwise_di…MeasureTheory.mem_fundamentalInterior · cited by 1MeasureTheory.mem_fundame…MeasureTheory.NullMeasurableSet.fundamentalInterior · cited by 1NullMeasurableSet.fundame…MeasureTheory.fundamentalFrontier_union_fundamentalInterior · cited by 1MeasureTheory.fundamental…MeasureTheory.IsFundamentalDomain.measure_fundamentalInterior · cited by 0IsFundamentalDomain.measu…MeasureTheory.sdiff_fundamentalFrontier · cited by 0MeasureTheory.sdiff_funda…MeasureTheory.sdiff_fundamentalInterior · cited by 0MeasureTheory.sdiff_funda…MeasureTheory.IsFundamentalDomain.fundamentalInterior · cited by 0IsFundamentalDomain.funda…MeasureTheory.fundamentalInterior_smul · cited by 0MeasureTheory.fundamental…MeasureTheory.fundamentalInterior_subset · cited by 0MeasureTheory.fundamental…MeasureTheory.fundamentalInterior_union_fundamentalFrontier · cited by 0MeasureTheory.fundamental…MeasureTheory.disjoint_fundamentalInterior_fundamentalFrontier · cited by 0MeasureTheory.disjoint_fu…Set · cited by 53352SetGroup · cited by 6238GroupSet.iUnion · cited by 2483Set.iUnionMulAction · cited by 1294MulActionMeasureTheory.fundamentalInte…CITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement and proof · cited by 53,352
  • Groupstatement and proof · cited by 6,238
  • Set.iUnionproof · cited by 2,483
  • MulActionstatement and proof · cited by 1,294

Cited by12

Results whose statement or proof uses this declaration.