Theorems · Definition · measure theory

MeasurableSup.casesOn

{M : Type u_1} →
  [inst : MeasurableSpace M] →
    [inst_1 : Max M] →
      {motive : MeasurableSup M → Sort u} →
        (t : MeasurableSup M) →
          ((measurable_const_sup : ∀ (c : M), Measurable fun x => c ⊔ x) →
              (measurable_sup_const : ∀ (c : M), Measurable fun x => x ⊔ c) → motive ⋯) →
            motive t

Defined in: Mathlib.MeasureTheory.Order.Lattice
Cited by: 0 results in Mathlib
Foundations: Depth 18 from the axioms · uses no axioms
Assumes: MeasurableSpace Max

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
MeasurableSupstatement and proof · cited by 18

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.