Documentation Verification Report

Real

📁 Source: Mathlib/Topology/Algebra/Ring/Real.lean

Statistics

Metric	Count
Definitions	0
Theorems `instContinuousAdd`, `instContinuousInv`, `isEmbedding_coe`, `isOpenEmbedding_coe`, `nhds_coe_coe`, `tendsto_coe`, `instContinuousNeg`, `instContinuousInv₀`, `instContinuousSMulOfReal`, `instContinuousSub`, `instIsTopologicalSemiring`, `uniformContinuous_add`, `uniformContinuous_const_mul`, `uniformContinuous_neg`, `instIsTopologicalAddGroupReal`, `instIsTopologicalDivisionRingReal`, `instIsTopologicalRingReal`, `instIsUniformAddGroupReal`, `instNoncompactSpaceReal`	19
Total	19

ENNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instContinuousAdd` 📖	mathematical	—	`ContinuousAdd` `ENNReal` `instTopologicalSpace` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiring`	—	`continuous_iff_continuousAt` `tendsto_nhds_top_mono'` `instOrderTopology` `continuousAt_fst` `le_add_right` `instCanonicallyOrderedAdd` `le_rfl` `continuousAt_snd` `le_add_left` `nhds_coe_coe` `IsTopologicalSemiring.toContinuousAdd` `NNReal.instIsTopologicalSemiring`
`instContinuousInv` 📖	mathematical	—	`ContinuousInv` `ENNReal` `instTopologicalSpace` `instInv`	—	`OrderIso.continuous` `instOrderTopology` `instOrderTopologyOrderDual`
`isEmbedding_coe` 📖	mathematical	—	`Topology.IsEmbedding` `NNReal` `ENNReal` `NNReal.instTopologicalSpace` `instTopologicalSpace` `ofNNReal`	—	`StrictMono.isEmbedding_of_ordConnected` `NNReal.instOrderTopology` `instOrderTopology` `coe_strictMono` `range_coe'` `Set.ordConnected_Iio`
`isOpenEmbedding_coe` 📖	mathematical	—	`Topology.IsOpenEmbedding` `NNReal` `ENNReal` `NNReal.instTopologicalSpace` `instTopologicalSpace` `ofNNReal`	—	`isEmbedding_coe` `range_coe'` `isOpen_Iio` `instClosedIciTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopology`
`nhds_coe_coe` 📖	mathematical	—	`nhds` `ENNReal` `instTopologicalSpaceProd` `instTopologicalSpace` `ofNNReal` `Filter.map` `NNReal` `NNReal.instTopologicalSpace`	—	`Topology.IsOpenEmbedding.map_nhds_eq` `Topology.IsOpenEmbedding.prodMap` `isOpenEmbedding_coe`
`tendsto_coe` 📖	mathematical	—	`Filter.Tendsto` `ENNReal` `ofNNReal` `nhds` `instTopologicalSpace` `NNReal` `NNReal.instTopologicalSpace`	—	`Topology.IsEmbedding.tendsto_nhds_iff` `isEmbedding_coe`

EReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instContinuousNeg` 📖	mathematical	—	`ContinuousNeg` `EReal` `instTopologicalSpace` `instNeg`	—	`OrderIso.continuous` `instOrderTopology` `instOrderTopologyOrderDual`

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instContinuousInv₀` 📖	mathematical	—	`ContinuousInv₀` `NNReal` `instZeroNNReal` `instInv` `instTopologicalSpace`	—	`IsStrictOrderedRing.toContinuousInv₀` `instIsStrictOrderedRing` `instOrderTopology` `IsTopologicalSemiring.toContinuousMul` `instIsTopologicalSemiring`
`instContinuousSMulOfReal` 📖	mathematical	—	`ContinuousSMul` `NNReal` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiringNNReal` `MulAction.toSemigroupAction` `instMulActionOfReal` `instTopologicalSpace`	—	`Continuous.smul` `Continuous.fst'` `continuous_induced_dom` `continuous_snd`
`instContinuousSub` 📖	mathematical	—	`ContinuousSub` `NNReal` `instTopologicalSpace` `instSub`	—	`Continuous.max` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `Continuous.fst'` `continuous_coe` `Continuous.snd'` `continuous_const`
`instIsTopologicalSemiring` 📖	mathematical	—	`IsTopologicalSemiring` `NNReal` `instTopologicalSpace` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`continuousAdd_induced` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `continuousMul_induced` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `IsTopologicalSemiring.toContinuousMul`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`uniformContinuous_add` 📖	mathematical	—	`UniformContinuous` `Real` `instUniformSpaceProd` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instAdd`	—	`Metric.uniformContinuous_iff` `rat_add_continuous_lemma` `instIsStrictOrderedRing` `IsAbsoluteValue.abs_isAbsoluteValue` `max_lt_iff`
`uniformContinuous_const_mul` 📖	mathematical	—	`UniformContinuous` `Real` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instMul`	—	`uniformContinuous_of_continuousAt_zero` `instIsUniformAddGroupReal` `AddMonoidHom.instAddMonoidHomClass` `Continuous.continuousAt` `ContinuousConstSMul.continuous_const_smul` `SMulCommClass.continuousConstSMul` `smulCommClass_self` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `IsStrictOrderedRing.toIsTopologicalDivisionRing` `instIsStrictOrderedRing` `instOrderTopologyReal`
`uniformContinuous_neg` 📖	mathematical	—	`UniformContinuous` `Real` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `instNeg`	—	`Metric.uniformContinuous_iff` `neg_sub_neg` `abs_sub_comm`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsTopologicalAddGroupReal` 📖	mathematical	—	`IsTopologicalAddGroup` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instAddGroup`	—	`LinearOrderedAddCommGroup.toIsTopologicalAddGroup` `Real.instIsOrderedAddMonoid` `instOrderTopologyReal`
`instIsTopologicalDivisionRingReal` 📖	mathematical	—	`IsTopologicalDivisionRing` `Real` `Real.instDivisionRing` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`IsStrictOrderedRing.toIsTopologicalDivisionRing` `Real.instIsStrictOrderedRing` `instOrderTopologyReal`
`instIsTopologicalRingReal` 📖	mathematical	—	`IsTopologicalRing` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Real.commRing`	—	`IsTopologicalDivisionRing.toIsTopologicalRing` `IsStrictOrderedRing.toIsTopologicalDivisionRing` `Real.instIsStrictOrderedRing` `instOrderTopologyReal`
`instIsUniformAddGroupReal` 📖	mathematical	—	`IsUniformAddGroup` `Real` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instAddGroup`	—	`IsUniformAddGroup.mk'` `Real.uniformContinuous_add` `Real.uniformContinuous_neg`
`instNoncompactSpaceReal` 📖	mathematical	—	`NoncompactSpace` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`Topology.IsClosedEmbedding.noncompactSpace` `instNoncompactSpaceInt` `Int.isClosedEmbedding_coe_real`

---

← Back to Index