Def MeasureTheory.SimpleFunc.ennrealRatEmbed

Modification history

2023-05-21 16:04

Mathlib/MeasureTheory/Function/SimpleFunc.lean

feat: port MeasureTheory.Function.SimpleFunc (#4043)

Added MeasureTheory.SimpleFunc.ennrealRatEmbed View on Github →