Documentation Verification Report

Paracompact

📁 Source: Mathlib/Topology/Compactness/Paracompact.lean

Statistics

Metric	Count
Definitions `ParacompactSpace`	1
Theorems `paracompactSpace_iff`, `locallyFinite_refinement`, `of_hasBasis`, `of_paracompactSpace_t2Space`, `paracompactSpace`, `instParacompactSpaceProdOfCompactSpace`, `instParacompactSpaceProdOfCompactSpace_1`, `paracompact_of_compact`, `paracompact_of_locallyCompact_sigmaCompact`, `precise_refinement`, `precise_refinement_set`, `refinement_of_locallyCompact_sigmaCompact_of_nhds_basis`, `refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set`	13
Total	14

Homeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`paracompactSpace_iff` 📖	mathematical	—	`ParacompactSpace`	—	`Topology.IsClosedEmbedding.paracompactSpace` `isClosedEmbedding`

ParacompactSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`locallyFinite_refinement` 📖	mathematical	`IsOpen` `Set.iUnion` `Set.univ`	`LocallyFinite` `Set` `Set.instHasSubset`	—	—
`of_hasBasis` 📖	mathematical	`Filter.HasBasis` `nhds` `IsOpen` `Set.iUnion` `Set.univ` `LocallyFinite` `Set` `Set.instHasSubset`	`ParacompactSpace`	—	`Filter.HasBasis.mem_iff` `IsOpen.mem_nhds` `Set.iUnion_eq_univ_iff` `Set.mem_range_self` `Set.forall_subtype_range_iff` `Set.iUnion_subtype` `Set.biUnion_range` `LocallyFinite.on_range` `HasSubset.Subset.trans` `Set.instIsTransSubset`

T4Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_paracompactSpace_t2Space` 📖	mathematical	—	`T4Space`	—	`precise_refinement_set` `Set.mem_iUnion` `isOpen_iUnion` `IsClosed.isOpen_compl` `isClosed_closure` `LocallyFinite.closure_iUnion` `Set.compl_iUnion` `Set.subset_iInter_iff` `closure_minimal` `Disjoint.le_bot` `isClosed_compl_iff` `Disjoint.mono` `le_rfl` `compl_le_compl` `subset_closure` `disjoint_compl_right` `SetCoe.forall'` `T2Space.t1Space` `t2_separation` `Disjoint.ne_of_mem` `Disjoint.symm` `Set.singleton_subset_iff`

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`paracompactSpace` 📖	mathematical	`Topology.IsClosedEmbedding`	`ParacompactSpace`	—	`precise_refinement_set` `isClosed_range` `IsOpen.preimage` `continuous` `LocallyFinite.preimage_continuous` `Set.preimage_mono` `Topology.IsInducing.isOpen_iff` `Topology.IsEmbedding.toIsInducing` `toIsEmbedding`

(root)

Definitions

Name	Category	Theorems
`ParacompactSpace` 📖	CompData	8 math math: `paracompact_of_compact`, `instParacompactSpaceProdOfCompactSpace`, `instParacompactSpaceProdOfCompactSpace_1`, `Topology.IsClosedEmbedding.paracompactSpace`, `Metric.instParacompactSpace`, `Homeomorph.paracompactSpace_iff`, `ParacompactSpace.of_hasBasis`, `paracompact_of_locallyCompact_sigmaCompact`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instParacompactSpaceProdOfCompactSpace` 📖	mathematical	—	`ParacompactSpace` `instTopologicalSpaceProd`	—	`isOpen_prod_iff` `Set.iUnion_eq_univ_iff` `isOpen_biInter_finset` `Set.mem_iInter₂` `precise_refinement` `IsOpen.prod` `Set.iUnion₂_eq_univ_iff` `prod_mem_nhds` `Filter.univ_mem` `Set.Finite.subset` `Set.Finite.biUnion` `Set.finite_range` `Finite.of_fintype` `Set.mem_iUnion₂` `Set.mem_range_self` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.prod_mono` `Set.Subset.rfl` `Set.iInter₂_subset` `CompactSpace.elim_nhds_subcover` `IsOpen.mem_nhds`
`instParacompactSpaceProdOfCompactSpace_1` 📖	mathematical	—	`ParacompactSpace` `instTopologicalSpaceProd`	—	`Homeomorph.paracompactSpace_iff` `instParacompactSpaceProdOfCompactSpace`
`paracompact_of_compact` 📖	mathematical	—	`ParacompactSpace`	—	`IsCompact.elim_finite_subcover` `isCompact_univ` `Eq.ge` `Set.iUnion_coe_set` `Set.iUnion_congr_Prop` `locallyFinite_of_finite` `Finite.of_fintype` `Set.Subset.rfl`
`paracompact_of_locallyCompact_sigmaCompact` 📖	mathematical	—	`ParacompactSpace`	—	`Filter.HasBasis.restrict_subset` `nhds_basis_opens` `IsOpen.mem_nhds` `refinement_of_locallyCompact_sigmaCompact_of_nhds_basis` `Set.iUnion_eq_univ_iff`
`precise_refinement` 📖	mathematical	`IsOpen` `Set.iUnion` `Set.univ`	`LocallyFinite` `Set` `Set.instHasSubset`	—	`ParacompactSpace.locallyFinite_refinement` `Set.mem_range_self` `Set.forall_subtype_range_iff` `Set.sUnion_range` `Subtype.range_coe` `isOpen_iUnion` `Set.Finite.subset` `Set.Finite.image` `Set.mem_image_of_mem`
`precise_refinement_set` 📖	mathematical	`IsOpen` `Set` `Set.instHasSubset` `Set.iUnion`	`LocallyFinite`	—	`Set.Subset.antisymm` `Set.subset_univ` `Set.compl_union_self` `Set.iUnion_option` `Set.union_subset_union_right` `precise_refinement` `isOpen_compl_iff` `Set.Subset.trans` `Set.subset_compl_comm` `LocallyFinite.comp_injective` `Option.some_injective`
`refinement_of_locallyCompact_sigmaCompact_of_nhds_basis` 📖	mathematical	`Filter.HasBasis` `nhds`	`Set.iUnion` `Set.univ` `LocallyFinite`	—	`refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set` `isClosed_univ` `Set.univ_subset_iff`
`refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set` 📖	mathematical	`Filter.HasBasis` `nhds`	`Set` `Set.instMembership` `Set.instHasSubset` `Set.iUnion` `LocallyFinite`	—	`CompactExhaustion.find_shiftr` `Set.diff_subset_diff_right` `interior_subset` `CompactExhaustion.mem_diff_shiftr_find` `IsCompact.inter_right` `IsCompact.diff` `CompactExhaustion.isCompact` `isOpen_interior` `IsClosed.compl_mem_nhds` `CompactExhaustion.isClosed` `CompactExhaustion.subset_interior_succ` `Filter.HasBasis.mem_of_mem` `Set.mem_iUnion` `Set.mem_iUnion₂` `IsOpen.mem_nhds` `Set.Finite.biUnion` `Set.finite_le_nat` `Set.finite_range` `Finite.of_fintype` `Set.Finite.subset` `Set.mem_compl_iff` `Mathlib.Tactic.Contrapose.contrapose₂` `CompactExhaustion.subset` `IsCompact.elim_nhds_subcover'` `Filter.HasBasis.mem_iff`

---

← Back to Index