Commit 2025-10-16 08:08 7065ce74

View on Github →

feat: Borel space on WithTop (#30543)

add untopA, abbreviation of untopD with Classical.arbitrary as default value
prove continuity of functions related to WithTop: coercion from the base type, untop, untopD, untopA
define the Borel measurable space on WithTop, and prove measurability of the same functions (from continuity)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Countable/Basic.lean

added theorem untopD_coe_enat

Created Mathlib/MeasureTheory/Constructions/BorelSpace/WithTop.lean

added theorem Measurable.untopA

added theorem Measurable.untopD

added theorem Measurable.withTop_coe

added def WithTop.MeasurableEquiv.neTopEquiv

added def WithTop.measurableEquivSum

added theorem WithTop.measurable_coe

added theorem WithTop.measurable_of_measurable_comp_coe

added theorem WithTop.measurable_untopA

added theorem WithTop.measurable_untopD

Modified Mathlib/Order/WithBot.lean

added theorem WithBot.unbotA_eq_unbot

added theorem WithTop.untopA_eq_untop

Modified Mathlib/Topology/Order/WithTop.lean

added theorem WithTop.continuousOn_untopA

added theorem WithTop.continuousOn_untopD

added theorem WithTop.continuous_coe

added theorem WithTop.continuous_untop

added theorem WithTop.isEmbedding_coe

added theorem WithTop.isOpenEmbedding_coe

added def WithTop.neTopHomeomorph

added theorem WithTop.nhds_coe

added def WithTop.sumHomeomorph

added theorem WithTop.tendsto_untop

added theorem WithTop.tendsto_untopA

added theorem WithTop.tendsto_untopD