Irreducible

📁 Source: Mathlib/Probability/Kernel/Irreducible.lean

Statistics

Metric	Count
Definitions IsIrreducible	1
Theorems irreducible, instIsIrreducibleHSMulENNRealMeasure, instIsIrreducibleIdOfSubsingleton, isIrreducible_iff, isIrreducible_of_le_measure	5
Total	6

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
IsIrreducible 📖	CompData	4 math math: isIrreducible_iff, instIsIrreducibleHSMulENNRealMeasure, instIsIrreducibleIdOfSubsingleton, isIrreducible_of_le_measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsIrreducibleHSMulENNRealMeasure 📖	mathematical	—	IsIrreducible ENNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	IsScalarTower.right IsIrreducible.irreducible ENNReal.instCanonicallyOrderedAdd ENNReal.instNoZeroDivisors
instIsIrreducibleIdOfSubsingleton 📖	mathematical	—	IsIrreducible id	—	Subsingleton.mem_iff_nonempty MeasureTheory.nonempty_of_measure_ne_zero ne_of_lt pow_one id_apply MeasureTheory.Measure.dirac_apply_of_mem IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero
isIrreducible_iff 📖	mathematical	—	IsIrreducible ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike Monoid.toNatPow instMonoid instZeroENNReal	—	—
isIrreducible_of_le_measure 📖	mathematical	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder MeasureTheory.Measure.instPartialOrder	IsIrreducible	—	IsIrreducible.irreducible instLawfulOrderLT_mathlib

ProbabilityTheory.Kernel.IsIrreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
irreducible 📖	mathematical	MeasurableSet ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike instZeroENNReal	ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike Monoid.toNatPow ProbabilityTheory.Kernel.instMonoid	—	—

---

← Back to Index