Lattice

📁 Source: Mathlib/MeasureTheory/Order/Group/Lattice.lean

Statistics

Metric	Count
Definitions	0
Theorems abs, mabs, abs, leOnePart, mabs, negPart, oneLePart, posPart, measurable_abs, measurable_leOnePart, measurable_mabs, measurable_negPart, measurable_oneLePart, measurable_posPart	14
Total	14

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs 📖	mathematical	AEMeasurable	abs	—	Measurable.comp_aemeasurable measurable_abs
mabs 📖	mathematical	AEMeasurable	mabs	—	Measurable.comp_aemeasurable measurable_mabs

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs 📖	mathematical	Measurable	abs	—	comp measurable_abs
leOnePart 📖	mathematical	Measurable	LeOnePart.leOnePart instLeOnePart	—	comp measurable_leOnePart
mabs 📖	mathematical	Measurable	mabs	—	comp measurable_mabs
negPart 📖	mathematical	Measurable	NegPart.negPart instNegPart	—	comp measurable_negPart
oneLePart 📖	mathematical	Measurable	OneLePart.oneLePart instOneLePart	—	comp measurable_oneLePart
posPart 📖	mathematical	Measurable	PosPart.posPart instPosPart	—	comp measurable_posPart

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_abs 📖	mathematical	—	Measurable abs	—	Measurable.sup measurable_id' MeasurableNeg.measurable_neg
measurable_leOnePart 📖	mathematical	—	Measurable LeOnePart.leOnePart instLeOnePart	—	Measurable.comp MeasurableSup.measurable_sup_const MeasurableInv.measurable_inv
measurable_mabs 📖	mathematical	—	Measurable mabs	—	Measurable.sup measurable_id' MeasurableInv.measurable_inv
measurable_negPart 📖	mathematical	—	Measurable NegPart.negPart instNegPart	—	Measurable.comp MeasurableSup.measurable_sup_const MeasurableNeg.measurable_neg
measurable_oneLePart 📖	mathematical	—	Measurable OneLePart.oneLePart instOneLePart	—	MeasurableSup.measurable_sup_const
measurable_posPart 📖	mathematical	—	Measurable PosPart.posPart instPosPart	—	MeasurableSup.measurable_sup_const

---

← Back to Index