Theorems · Theorem · measure theory

AddCircle.volume_of_add_preimage_eq

∀ {T : ℝ} [hT : Fact (0 < T)] (s I : Set (AddCircle T)) (u x : AddCircle T),
  IsOfFinAddOrder u →
    u +ᵥ s =ᵐ[MeasureTheory.volume] s →
      I =ᵐ[MeasureTheory.volume] Metric.ball x (T / (2 * ↑(addOrderOf u))) →
        MeasureTheory.volume s = addOrderOf u • MeasureTheory.volume (s ∩ I)

Defined in: Mathlib.MeasureTheory.Group.AddCircle
Cited by: 1 results in Mathlib
Foundations: Depth 251 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fact

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites24

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

DFunLike.coestatement and proof · cited by 62,936
Setstatement and proof · cited by 53,352
Realstatement and proof · cited by 25,697
MeasureTheory.Measurestatement · cited by 10,939
ENNRealstatement and proof · cited by 9,879
Fintypeproof · cited by 7,736
AddSubgroupproof · cited by 3,232
Factstatement and proof · cited by 2,726
MeasureTheory.aestatement and proof · cited by 2,352
Filter.EventuallyEqstatement and proof · cited by 1,912
HVAdd.hVAddstatement and proof · cited by 1,820
MeasureTheory.MeasureSpace.volumestatement and proof · cited by 1,323

Cited by1

Results whose statement or proof uses this declaration.

AddCircle.ae_empty_or_univ_of_forall_vadd_ae_eq_selfproof · cited by 2