Documentation Verification Report

WithTop

📁 Source: Mathlib/MeasureTheory/Constructions/BorelSpace/WithTop.lean

Statistics

Metric	Count
Definitions `neTopEquiv`, `instMeasurableSpace`, `measurableEquivSum`	3
Theorems `untopA`, `untopD`, `withTop_coe`, `instBorelSpace`, `measurable_coe`, `measurable_of_measurable_comp_coe`, `measurable_untopA`, `measurable_untopD`	8
Total	11

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`untopA` 📖	mathematical	`Measurable` `WithTop` `WithTop.instMeasurableSpace`	`WithTop.untopA`	—	`untopD`
`untopD` 📖	mathematical	`Measurable` `WithTop` `WithTop.instMeasurableSpace`	`WithTop.untopD`	—	`comp` `WithTop.measurable_untopD`
`withTop_coe` 📖	mathematical	`Measurable`	`WithTop` `WithTop.instMeasurableSpace` `WithTop.some`	—	`comp` `WithTop.measurable_coe`

WithTop

Definitions

Name	Category	Theorems
`instMeasurableSpace` 📖	CompOp	9 math math: `measurable_coe`, `instBorelSpace`, `measurable_untopA`, `MeasureTheory.IsStoppingTime.measurable`, `MeasureTheory.IsStoppingTime.measurable'`, `measurable_of_measurable_comp_coe`, `Measurable.withTop_coe`, `measurable_untopD`, `MeasureTheory.IsStoppingTime.measurable_of_le`
`measurableEquivSum` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instBorelSpace` 📖	mathematical	—	`BorelSpace` `WithTop` `TopologicalSpace.instWithTopOfOrderTopology` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instMeasurableSpace`	—	—
`measurable_coe` 📖	mathematical	—	`Measurable` `WithTop` `instMeasurableSpace` `some`	—	`Continuous.measurable` `BorelSpace.opensMeasurable` `instBorelSpace` `continuous_coe`
`measurable_of_measurable_comp_coe` 📖	mathematical	`Measurable` `some`	`WithTop` `instMeasurableSpace`	—	`measurable_of_measurable_on_compl_singleton` `OpensMeasurableSpace.toMeasurableSingletonClass` `BorelSpace.opensMeasurable` `instBorelSpace` `T5Space.toT1Space` `OrderTopology.t5Space` `TopologicalSpace.instOrderTopologyWithTop` `MeasurableEquiv.measurable_comp_iff`
`measurable_untopA` 📖	mathematical	—	`Measurable` `WithTop` `instMeasurableSpace` `untopA`	—	`measurable_untopD`
`measurable_untopD` 📖	mathematical	—	`Measurable` `WithTop` `instMeasurableSpace` `untopD`	—	`measurable_of_measurable_comp_coe` `measurable_id`

WithTop.MeasurableEquiv

Definitions

Name	Category	Theorems
`neTopEquiv` 📖	CompOp	—

---

← Back to Index