Theorems · Definition · measure theory

MeasureTheory.SimpleFunc.piecewise

{α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      (s : Set α) →
        MeasurableSet s → MeasureTheory.SimpleFunc α β → MeasureTheory.SimpleFunc α β → MeasureTheory.SimpleFunc α β

If-then-else as a SimpleFunc.

Defined in: Mathlib.MeasureTheory.Function.SimpleFunc
Cited by: 26 results in Mathlib
Foundations: Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites6

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

DFunLike.coeproof · cited by 62,936
Setstatement and proof · cited by 53,352
MeasurableSpacestatement and proof · cited by 13,106
MeasurableSetstatement and proof · cited by 3,075
MeasureTheory.SimpleFuncstatement and proof · cited by 411
Set.piecewiseproof · cited by 136

Cited by28

Results whose statement or proof uses this declaration.

MeasureTheory.SimpleFunc.restrictproof · cited by 25
MeasureTheory.SimpleFunc.inductionstatement and proof · cited by 14
MeasureTheory.Lp.simpleFunc.indicatorConstproof · cited by 14
MeasureTheory.StronglyMeasurable.piecewiseproof · cited by 6
MeasureTheory.SimpleFunc.piecewise_samestatement · cited by 6
MeasureTheory.SimpleFunc.piecewise.congr_simpstatement and proof · cited by 4
MeasureTheory.SimpleFunc.measure_lt_top_of_memLp_indicatorstatement and proof · cited by 3
MeasureTheory.SimpleFunc.piecewise_univstatement · cited by 2
MeasureTheory.Lp.simpleFunc.inductionproof · cited by 2
MeasureTheory.MemLp.induction_denseproof · cited by 2
MeasureTheory.SimpleFunc.piecewise_emptystatement · cited by 2
MeasureTheory.SimpleFunc.coe_piecewisestatement · cited by 1