Documentation Verification Report

ClosedCompactCylinders

📁 Source: Mathlib/MeasureTheory/Constructions/ClosedCompactCylinders.lean

Statistics

Metric	Count
Definitions `closedCompactCylinders`, `finset`	2
Theorems `eq_cylinder`, `isClosed`, `isCompact`, `cylinder_mem_closedCompactCylinders`, `empty_mem_closedCompactCylinders`, `mem_closedCompactCylinders`, `mem_measurableCylinders_of_mem_closedCompactCylinders`	7
Total	9

MeasureTheory

Definitions

Name	Category	Theorems
`closedCompactCylinders` 📖	CompOp	3 math math: `mem_closedCompactCylinders`, `empty_mem_closedCompactCylinders`, `cylinder_mem_closedCompactCylinders`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cylinder_mem_closedCompactCylinders` 📖	mathematical	`IsCompact` `Pi.topologicalSpace` `Finset` `SetLike.instMembership` `Finset.instSetLike`	`Set` `Set.instMembership` `closedCompactCylinders` `cylinder`	—	`mem_closedCompactCylinders`
`empty_mem_closedCompactCylinders` 📖	mathematical	—	`Set` `Set.instMembership` `closedCompactCylinders` `Set.instEmptyCollection`	—	`isClosed_empty` `isCompact_empty` `cylinder_empty`
`mem_closedCompactCylinders` 📖	mathematical	—	`Set` `Set.instMembership` `closedCompactCylinders` `IsClosed` `Pi.topologicalSpace` `Finset` `SetLike.instMembership` `Finset.instSetLike` `IsCompact` `cylinder`	—	—
`mem_measurableCylinders_of_mem_closedCompactCylinders` 📖	mathematical	`SecondCountableTopology` `OpensMeasurableSpace` `Set` `Set.instMembership` `closedCompactCylinders`	`measurableCylinders`	—	`mem_measurableCylinders` `IsClosed.measurableSet` `Pi.opensMeasurableSpace` `Finite.to_countable` `Finite.of_fintype` `closedCompactCylinders.isClosed` `closedCompactCylinders.eq_cylinder`

MeasureTheory.closedCompactCylinders

Definitions

Name	Category	Theorems
`finset` 📖	CompOp	3 math math: `isCompact`, `eq_cylinder`, `isClosed`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_cylinder` 📖	mathematical	`Set` `Set.instMembership` `MeasureTheory.closedCompactCylinders`	`MeasureTheory.cylinder` `finset` `set`	—	`MeasureTheory.mem_closedCompactCylinders`
`isClosed` 📖	mathematical	`Set` `Set.instMembership` `MeasureTheory.closedCompactCylinders`	`IsClosed` `Pi.topologicalSpace` `Finset` `SetLike.instMembership` `Finset.instSetLike` `finset` `set`	—	`MeasureTheory.mem_closedCompactCylinders`
`isCompact` 📖	mathematical	`Set` `Set.instMembership` `MeasureTheory.closedCompactCylinders`	`IsCompact` `Pi.topologicalSpace` `Finset` `SetLike.instMembership` `Finset.instSetLike` `finset` `set`	—	`MeasureTheory.mem_closedCompactCylinders`

---

← Back to Index