Packages that do use the axioms of mesure theory

Stream: general

[Bilel Methnani]

Hello everyone, I am new to lean. It would be very helpful to me if you can tell me what packages in mathlib that do use the axiom of mesure theory. thank you.

[Aaron Liu]

what is the "axioms of measure theory"

[Bilel Methnani]

Kolmogorov's Axioms for Measures

[Aaron Liu]

do you mean the like fields of docs#MeasureTheory.Measure

[Bilel Methnani]

yes, if i use any lemma of this package would that be assuming the axioms ?

[Aaron Liu]

there's not any axioms in the sense of axiom

[Aaron Liu]

these are more like requirements for something to be a measure

[Riccardo Brasca]

You can read this for a basic introduction to probability theory in mathlib.