Documentation Verification Report

Pi

📁 Source: Mathlib/Topology/EMetricSpace/Pi.lean

Statistics

Metric	Count
Definitions `emetricSpacePi`, `instEDistForall`, `pseudoEMetricSpacePi`	3
Theorems `edist_le_pi_edist`, `edist_pi_const`, `edist_pi_const_le`, `edist_pi_def`, `edist_pi_le_iff`	5
Total	8

(root)

Definitions

Name	Category	Theorems
`emetricSpacePi` 📖	CompOp	7 math math: `MeasureTheory.hausdorffMeasure_measurePreserving_piFinTwo`, `Real.dimH_univ_pi_fin`, `Real.dimH_ball_pi`, `MeasureTheory.hausdorffMeasure_pi_real`, `MeasureTheory.hausdorffMeasure_measurePreserving_funUnique`, `Real.dimH_univ_pi`, `Real.dimH_ball_pi_fin`
`instEDistForall` 📖	CompOp	8 math math: `edist_le_pi_edist`, `UniformOnFun.edist_eq_pi_restrict`, `edist_pi_le_iff`, `edist_pi_const_le`, `edist_pi_def`, `edist_pi_const`, `Fin.edist_append_eq_max_edist`, `Set.le_einfsep_pi_of_le`
`pseudoEMetricSpacePi` 📖	CompOp	33 math math: `PiLp.lipschitzWith_toLp`, `IsometryEquiv.sumArrowIsometryEquivProdArrow_toHomeomorph`, `Isometry.single`, `Pi.isIsometricVAdd'`, `EMetric.diam_pi_le_of_le`, `IsometryEquiv.piCongrLeft'_apply`, `Fin.appendIsometry_symm_apply`, `PiLp.antilipschitzWith_toLp`, `Pi.isIsometricSMul''`, `Isometry.piMap`, `instIsIsometricSMulForall`, `Fin.appendIsometryOfEq_apply`, `Pi.isIsometricSMul'`, `PiLp.lipschitzWith_ofLp`, `Metric.ediam_pi_le_of_le`, `IsometryEquiv.piFinTwo_symm_apply`, `Fin.appendIsometry_toHomeomorph`, `IsometryEquiv.sumArrowIsometryEquivProdArrow_symm_apply`, `IsometryEquiv.piCongrLeft_symm_apply`, `IsometryEquiv.funUnique_apply`, `PiLp.antilipschitzWith_ofLp`, `IsometryEquiv.piCongrLeft_apply`, `Fin.appendIsometryOfEq_symm_apply`, `LipschitzWith.eval`, `IsometryEquiv.piCongrLeft'_symm_apply`, `Real.volume_pi_le_diam_pow`, `instIsIsometricVAddForall`, `IsometryEquiv.funUnique_symm_apply`, `PiLp.isometry_ofLp_infty`, `IsometryEquiv.piFinTwo_apply`, `Fin.appendIsometry_apply`, `Pi.isIsometricVAdd''`, `IsometryEquiv.sumArrowIsometryEquivProdArrow_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`edist_le_pi_edist` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `instEDistForall`	—	`Finset.le_sup` `Finset.mem_univ`
`edist_pi_const` 📖	mathematical	—	`EDist.edist` `instEDistForall` `PseudoEMetricSpace.toEDist`	—	`Finset.sup_const` `Finset.univ_nonempty`
`edist_pi_const_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `instEDistForall` `PseudoEMetricSpace.toEDist`	—	`edist_pi_le_iff` `le_rfl`
`edist_pi_def` 📖	mathematical	—	`EDist.edist` `instEDistForall` `Finset.sup` `ENNReal` `instSemilatticeSupENNReal` `ENNReal.instOrderBot` `Finset.univ`	—	—
`edist_pi_le_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `instEDistForall`	—	`Finset.sup_le_iff`

---

← Back to Index