Skip to content

[Merged by Bors] - feat: the identity function is a.e.-strongly measurable w.r.t. the map by an a.e.-strongly measurable function#39644

Closed
EtienneC30 wants to merge 3 commits into
leanprover-community:masterfrom
EtienneC30:asm_id
Closed

[Merged by Bors] - feat: the identity function is a.e.-strongly measurable w.r.t. the map by an a.e.-strongly measurable function#39644
EtienneC30 wants to merge 3 commits into
leanprover-community:masterfrom
EtienneC30:asm_id

remove measurability hypothesis

605d321
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
post-or-update-summary-comment
succeeded May 21, 2026 in 1m 15s