Documentation Verification Report

LocallyContractible

📁 Source: Mathlib/Topology/Homotopy/LocallyContractible.lean

Statistics

Metric	Count
Definitions `LocallyContractibleSpace`, `StronglyLocallyContractibleSpace`	2
Theorems `stronglyLocallyContractibleSpace`, `contractible_basis`, `locallyContractible`, `of_bases`, `stronglyLocallyContractibleSpace`, `contractible_subset_basis`, `instLocPathConnectedSpace`, `instStronglyLocallyContractibleSpaceProd`	8
Total	10

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`stronglyLocallyContractibleSpace` 📖	mathematical	`IsOpen`	`StronglyLocallyContractibleSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`Topology.IsOpenEmbedding.stronglyLocallyContractibleSpace` `isOpenEmbedding_subtypeVal`

StronglyLocallyContractibleSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contractible_basis` 📖	mathematical	—	`Filter.HasBasis` `Set` `nhds` `Filter` `Filter.instMembership` `ContractibleSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set.instMembership`	—	—
`locallyContractible` 📖	mathematical	—	`LocallyContractibleSpace`	—	`Filter.HasBasis.mem_iff` `contractible_basis` `id_nullhomotopic` `ContinuousMap.ext` `ContinuousMap.comp_id` `ContinuousMap.Homotopic.comp` `ContinuousMap.Homotopic.refl`
`of_bases` 📖	mathematical	`Filter.HasBasis` `nhds` `ContractibleSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	`StronglyLocallyContractibleSpace`	—	`Filter.hasBasis_self` `Filter.HasBasis.mem_iff` `Filter.HasBasis.mem_of_mem`

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`stronglyLocallyContractibleSpace` 📖	mathematical	`Topology.IsOpenEmbedding`	`StronglyLocallyContractibleSpace`	—	`StronglyLocallyContractibleSpace.of_bases` `Topology.IsInducing.basis_nhds` `Topology.IsEmbedding.toIsInducing` `toIsEmbedding` `contractible_subset_basis` `isOpen_range` `Set.mem_range_self` `Homeomorph.contractibleSpace_iff`

(root)

Definitions

Name	Category	Theorems
`LocallyContractibleSpace` 📖	MathDef	1 math math: `StronglyLocallyContractibleSpace.locallyContractible`
`StronglyLocallyContractibleSpace` 📖	CompData	4 math math: `Topology.IsOpenEmbedding.stronglyLocallyContractibleSpace`, `instStronglyLocallyContractibleSpaceProd`, `StronglyLocallyContractibleSpace.of_bases`, `IsOpen.stronglyLocallyContractibleSpace`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contractible_subset_basis` 📖	mathematical	`IsOpen` `Set` `Set.instMembership`	`Filter.HasBasis` `nhds` `Filter` `Filter.instMembership` `ContractibleSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set.instHasSubset`	—	`Filter.HasBasis.hasBasis_self_subset` `StronglyLocallyContractibleSpace.contractible_basis` `IsOpen.mem_nhds`
`instLocPathConnectedSpace` 📖	mathematical	—	`LocPathConnectedSpace`	—	`Filter.HasBasis.to_hasBasis'` `StronglyLocallyContractibleSpace.contractible_basis` `isPathConnected_iff_pathConnectedSpace` `ContractibleSpace.instPathConnectedSpace` `le_rfl`
`instStronglyLocallyContractibleSpaceProd` 📖	mathematical	—	`StronglyLocallyContractibleSpace` `instTopologicalSpaceProd`	—	`StronglyLocallyContractibleSpace.of_bases` `nhds_prod_eq` `Filter.HasBasis.prod` `StronglyLocallyContractibleSpace.contractible_basis` `Homeomorph.contractibleSpace` `ContractibleSpace.instProd`

---

← Back to Index