Commit 2025-03-11 16:38 1505c736

View on Github →

feat(MeasureTheory): cylinders with closed compact bases (#22688) Part of the formalization of Kolmogorov's extension theorem.

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Constructions/ClosedCompactCylinders.lean

added theorem MeasureTheory.closedCompactCylinders.eq_cylinder

added theorem MeasureTheory.closedCompactCylinders.isClosed

added theorem MeasureTheory.closedCompactCylinders.isCompact

added def MeasureTheory.closedCompactCylinders.set

added def MeasureTheory.closedCompactCylinders

added theorem MeasureTheory.cylinder_mem_closedCompactCylinders

added theorem MeasureTheory.empty_mem_closedCompactCylinders

added theorem MeasureTheory.mem_closedCompactCylinders

added theorem MeasureTheory.mem_measurableCylinders_of_mem_closedCompactCylinders