Repository navigation

feat: the essential supremum of a family of ℝ≥0∞-valued functions - #400

Merged

lmlexplore-automation[bot] merged 2 commits into

LeanMachineLearning:mainfrom

RemyDegenne:roadmap/exists-esssup-family-worker1

Nov 15, 2026

Merged

feat: the essential supremum of a family of ℝ≥0∞-valued functions#400
lmlexplore-automation[bot] merged 2 commits into
LeanMachineLearning:mainfrom
RemyDegenne:roadmap/exists-esssup-family-worker1

Commits on Nov 15, 2026
- feat: the essential supremum of a family of ℝ≥0∞-valued functions
  
  RemyDegenne
  and
  web-flow
  committed
  c262bd8
- docs: state the a.e.-measurability hypothesis in the essSupFamily overview
  
  RemyDegenne
  and
  web-flow
  committed
  467d665