1.4. ForMathlib.MeasureTheory.Order.Lattice🔗

Measurable inf of a finite set

Module LeanMachineLearning.ForMathlib.MeasureTheory.Order.Lattice contains 1 exposed declarations.

• Finset.measurable_inf'Theorem · 0 deps