Real

📁 Source: Mathlib/Topology/Bornology/Real.lean

Statistics

Metric	Count
Definitions	0
Theorems instIsOrderBornology, instOrderTopology, instIsOrderBornology	3
Total	3

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsOrderBornology 📖	mathematical	—	IsOrderBornology NNReal PseudoMetricSpace.toBornology instPseudoMetricSpaceNNReal PartialOrder.toPreorder instPartialOrderNNReal	—	IsOrderBornology.of_isCompactIcc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopology le_or_gt closedBall_zero_eq_Icc Metric.closedBall_of_neg
instOrderTopology 📖	mathematical	—	OrderTopology NNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instPseudoMetricSpaceNNReal PartialOrder.toPreorder instPartialOrderNNReal	—	orderTopology_of_ordConnected instOrderTopologyReal Set.ordConnected_Ici

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsOrderBornology 📖	mathematical	—	IsOrderBornology Real PseudoMetricSpace.toBornology pseudoMetricSpace instPreorder	—	IsOrderBornology.of_isCompactIcc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal closedBall_eq_Icc zero_sub zero_add

---

← Back to Index