Piecewise

📁 Source: Mathlib/MeasureTheory/Function/Piecewise.lean

Statistics

Metric	Count
Definitions simpleFunc_piecewise	1
Theorems aemeasurable_piecewise, aestronglyMeasurable_piecewise, measurable_piecewise, stronglyMeasurable_piecewise	4
Total	5

IndexedPartition

Definitions

Name	Category	Theorems
simpleFunc_piecewise 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_piecewise 📖	mathematical	MeasurableSet AEMeasurable	piecewise	—	MeasureTheory.Measure.instOuterMeasureClass measurable_piecewise Filter.mp_mem MeasureTheory.ae_all_iff Filter.univ_mem'
aestronglyMeasurable_piecewise 📖	mathematical	MeasurableSet MeasureTheory.AEStronglyMeasurable	piecewise	—	MeasureTheory.Measure.instOuterMeasureClass stronglyMeasurable_piecewise Filter.mp_mem MeasureTheory.ae_all_iff Filter.univ_mem'
measurable_piecewise 📖	mathematical	MeasurableSet Measurable	piecewise	—	piecewise_preimage MeasurableSet.iUnion MeasurableSet.inter
stronglyMeasurable_piecewise 📖	mathematical	MeasurableSet MeasureTheory.StronglyMeasurable	piecewise	—	exists_true_iff_nonempty nonempty_equiv_of_countable instCountableNat instInfiniteNat Equiv.injective EquivLike.toEmbeddingLike Finite.of_fintype MeasurableSet.biUnion Set.to_countable SetCoe.countable Equiv.bijective Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat EmbeddingLike.apply_eq_iff_eq mem_iff_index_eq Set.iUnion_congr_Prop Filter.mp_mem Filter.univ_mem' Filter.tendsto_congr'

---

← Back to Index