Real

📁 Source: Mathlib/Topology/MetricSpace/ProperSpace/Real.lean

Statistics

Metric	Count
Definitions	0
Theorems instSecondCountableTopology, instSecondCountableTopology, instProperSpace, instSecondCountableTopology	4
Total	4

ENNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSecondCountableTopology 📖	mathematical	—	SecondCountableTopology ENNReal instTopologicalSpace	—	Topology.IsEmbedding.secondCountableTopology instOrderTopology orderTopology_of_ordConnected instOrderTopologyReal Set.ordConnected_Icc TopologicalSpace.Subtype.secondCountableTopology instSecondCountableTopologyReal Homeomorph.isEmbedding

EReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSecondCountableTopology 📖	mathematical	—	SecondCountableTopology EReal instTopologicalSpace	—	Set.countable_range Encodable.countable denseRange_ratCast SecondCountableTopology.of_separableSpace_orderTopology instOrderTopology instDenselyOrderedEReal

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instProperSpace 📖	mathematical	—	ProperSpace NNReal instPseudoMetricSpaceNNReal	—	Isometry.isClosedEmbedding instCompleteSpace Topology.IsClosedEmbedding.isCompact_preimage ProperSpace.isCompact_closedBall instProperSpaceReal
instSecondCountableTopology 📖	mathematical	—	SecondCountableTopology NNReal instTopologicalSpace	—	TopologicalSpace.Subtype.secondCountableTopology instSecondCountableTopologyReal

---

← Back to Index