Theorems · Definition · measure theory

MeasurableSub.recOn

{G : Type u_2} →
  [inst : MeasurableSpace G] →
    [inst_1 : Sub G] →
      {motive : MeasurableSub G → Sort u} →
        (t : MeasurableSub G) →
          ((measurable_const_sub : ∀ (c : G), Measurable fun x => c - x) →
              (measurable_sub_const : ∀ (c : G), Measurable fun x => x - c) → motive ⋯) →
            motive t

Defined in: Mathlib.MeasureTheory.Group.Arithmetic
Cited by: 0 results in Mathlib
Foundations: Depth 11 from the axioms · uses no axioms
Assumes: MeasurableSpace Sub

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites3

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

MeasurableSpacestatement and proof · cited by 13,106
Measurablestatement and proof · cited by 1,499
MeasurableSubstatement and proof · cited by 8

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.