Documentation Verification Report

Sequence

📁 Source: Mathlib/Topology/Category/LightProfinite/Sequence.lean

Statistics

Metric	Count
Definitions `NatUnionInfty`, `instCoeNatCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyNatUnionInfty`, `natUnionInftyEmbedding`, `«termℕ∪{∞}»`	4
Theorems `continuous_iff_convergent`, `instMetrizableSpaceOnePointNat`, `isClosedEmbedding_natUnionInftyEmbedding`	3
Total	7

LightProfinite

Definitions

Name	Category	Theorems
`NatUnionInfty` 📖	CompOp	1 math math: `continuous_iff_convergent`
`instCoeNatCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyNatUnionInfty` 📖	CompOp	—
`natUnionInftyEmbedding` 📖	CompOp	1 math math: `isClosedEmbedding_natUnionInftyEmbedding`
`«termℕ∪{∞}»`»} 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_iff_convergent` 📖	mathematical	—	`Continuous` `TopCat.carrier` `CompHausLike.toTop` `TotallyDisconnectedSpace` `TopCat.str` `SecondCountableTopology` `NatUnionInfty` `OnePoint.instTopologicalSpace` `instTopologicalSpaceNat` `Filter.Tendsto` `OnePoint.some` `Filter.atTop` `Nat.instPreorder` `nhds` `OnePoint.infty`	—	`OnePoint.continuous_iff_from_nat`
`instMetrizableSpaceOnePointNat` 📖	mathematical	—	`TopologicalSpace.MetrizableSpace` `OnePoint` `OnePoint.instTopologicalSpace` `instTopologicalSpaceNat`	—	`Topology.IsEmbedding.metrizableSpace` `EMetricSpace.metrizableSpace` `Topology.IsClosedEmbedding.toIsEmbedding` `isClosedEmbedding_natUnionInftyEmbedding`
`isClosedEmbedding_natUnionInftyEmbedding` 📖	mathematical	—	`Topology.IsClosedEmbedding` `OnePoint` `Real` `OnePoint.instTopologicalSpace` `instTopologicalSpaceNat` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `natUnionInftyEmbedding`	—	`Topology.IsClosedEmbedding.of_continuous_injective_isClosedMap` `ContinuousMap.continuous` `Nat.cast_zero` `Nat.cast_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `one_div` `AddRightCancelSemigroup.toIsRightCancelAdd` `IsCompact.isClosed` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `IsCompact.image` `IsClosed.isCompact` `OnePoint.instCompactSpace`

---

← Back to Index