Commit 2023-05-22 18:01 1c2bf60a

View on Github →

feat: port MeasureTheory.Integral.RieszMarkovKakutani (#4195)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/RieszMarkovKakutani.lean

added theorem exists_lt_rieszContentAux_add_pos

added def rieszContentAux

added theorem rieszContentAux_le

added theorem rieszContentAux_mono

added theorem rieszContentAux_sup_le

added theorem riesz_content_aux_image_nonempty