Documentation Verification Report

Basic

📁 Source: Mathlib/Topology/Covering/Basic.lean

Statistics

Metric	Count
Definitions `IsCoveringMap`, `IsCoveringMapOn`, `IsEvenlyCovered`, `fiberHomeomorph`, `toTrivialization`, `toTrivialization'`, `trivializationDiscrete`	7
Theorems `isCoveringMap`, `isCoveringMapOn_of_openPartialHomeomorph`, `isEvenlyCovered_of_openPartialHomeomorph`, `comp_homeomorph`, `comp_homeomorph_iff`, `constOn_of_comp`, `const_of_comp`, `continuous`, `eqOn_of_comp_eqOn`, `eq_of_comp_eq`, `homeomorph_comp`, `homeomorph_comp_iff`, `isCoveringMapOn`, `isLocalHomeomorph`, `isOpenMap`, `isQuotientMap`, `isSeparatedMap`, `mk`, `mk'`, `of_discreteTopology`, `of_isEmpty`, `restrictPreimage`, `comp_homeomorph`, `comp_homeomorph_iff`, `continuousAt`, `continuousOn`, `homeomorph_comp`, `homeomorph_comp_iff`, `isCoveringMap_restrictPreimage`, `isLocalHomeomorphOn`, `mk`, `mk'`, `mono`, `of_isCoveringMap_restrictPreimage`, `of_isCoveringMap_subtype`, `of_isEmpty`, `of_openPartialHomeomorph`, `restrictPreimage`, `of_openPartialHomeomorph`, `comp_homeomorph`, `comp_homeomorph_iff`, `comp_subtypeVal`, `continuousAt`, `discreteTopology_fiber`, `homeomorph_comp`, `homeomorph_comp_iff`, `mem_toTrivialization_baseSet`, `of_fiber_homeomorph`, `of_openPartialHomeomorph`, `of_preimage_eq_empty`, `of_trivialization`, `restrictPreimage`, `subtypeVal_comp`, `toTrivialization_apply`, `to_isEvenlyCovered_preimage`, `isCoveringMap`, `trivializationDiscrete_baseSet`, `trivializationDiscrete_source`, `trivializationDiscrete_target`, `isCoveringMap_iff_isCoveringMapOn_univ`	60
Total	67

FiberBundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoveringMap` 📖	mathematical	—	`IsCoveringMap` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	—	`IsFiberBundle.isCoveringMap` `mem_baseSet_trivializationAt`

IsClosedMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoveringMapOn_of_openPartialHomeomorph` 📖	mathematical	`IsClosedMap` `Set.Finite` `Set.preimage` `Set` `Set.instSingletonSet` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `OpenPartialHomeomorph.toFun'`	`IsCoveringMapOn`	—	`isEvenlyCovered_of_openPartialHomeomorph`
`isEvenlyCovered_of_openPartialHomeomorph` 📖	mathematical	`IsClosedMap` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `OpenPartialHomeomorph.toFun'`	`IsEvenlyCovered` `Set.Elem` `Set.preimage` `Set.instSingletonSet` `instTopologicalSpaceSubtype`	—	`IsDiscrete.to_subtype` `IsDiscrete.of_openPartialHomeomorph` `subset_rfl` `Set.instReflSubset` `Set.Finite.t2_separation` `IsOpen.inter` `OpenPartialHomeomorph.open_source` `IsOpen.mem_nhdsSet` `isOpen_iUnion` `Set.mem_iUnion_of_mem` `isClosedMap_iff_comap_nhds_le` `isEmpty_or_nonempty` `IsEvenlyCovered.of_preimage_eq_empty` `Set.iUnion_of_empty` `mem_nhds_iff` `isOpen_iInter_of_finite` `Set.image_congr` `OpenPartialHomeomorph.isOpen_image_of_subset_source` `Set.inter_subset_right` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.iInter_subset` `IsEvenlyCovered.of_trivialization` `Set.inter_isAssoc` `Set.inter_isComm` `OpenPartialHomeomorph.isOpen_inter_preimage` `OpenPartialHomeomorph.image_source_eq_target` `Set.image_mono` `OpenPartialHomeomorph.isOpen_symm_image_iff_of_subset_target` `OpenPartialHomeomorph.symm_image_eq_source_inter_preimage` `Set.inter_comm` `Set.inter_eq_inter_iff_left` `Set.mem_iInter` `OpenPartialHomeomorph.injOn` `Set.InjOn.mono` `Set.SurjOn.mono` `Set.surjOn_image` `pairwise_disjoint_mono` `Set.Pairwise.subtype` `Set.inter_subset_left` `Set.preimage_mono`

IsCoveringMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_homeomorph` 📖	mathematical	`IsCoveringMap`	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`isCoveringMap_iff_isCoveringMapOn_univ` `IsCoveringMapOn.comp_homeomorph`
`comp_homeomorph_iff` 📖	mathematical	—	`IsCoveringMap` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`Homeomorph.apply_symm_apply` `comp_homeomorph`
`constOn_of_comp` 📖	—	`IsCoveringMap` `IsPreconnected` `ContinuousOn` `Set` `Set.instMembership`	—	—	`IsSeparatedMap.constOn_of_comp` `isSeparatedMap` `IsLocalHomeomorph.isLocallyInjective` `isLocalHomeomorph`
`const_of_comp` 📖	—	`IsCoveringMap` `Continuous`	—	—	`IsSeparatedMap.const_of_comp` `isSeparatedMap` `IsLocalHomeomorph.isLocallyInjective` `isLocalHomeomorph`
`continuous` 📖	mathematical	`IsCoveringMap`	`Continuous`	—	`continuousOn_univ` `IsCoveringMapOn.continuousOn` `isCoveringMapOn`
`eqOn_of_comp_eqOn` 📖	—	`IsCoveringMap` `IsPreconnected` `ContinuousOn` `Set.EqOn` `Set` `Set.instMembership`	—	—	`IsSeparatedMap.eqOn_of_comp_eqOn` `isSeparatedMap` `IsLocalHomeomorph.isLocallyInjective` `isLocalHomeomorph`
`eq_of_comp_eq` 📖	—	`IsCoveringMap` `Continuous`	—	—	`IsSeparatedMap.eq_of_comp_eq` `isSeparatedMap` `IsLocalHomeomorph.isLocallyInjective` `isLocalHomeomorph`
`homeomorph_comp` 📖	mathematical	`IsCoveringMap`	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`isCoveringMap_iff_isCoveringMapOn_univ` `IsCoveringMapOn.homeomorph_comp`
`homeomorph_comp_iff` 📖	mathematical	—	`IsCoveringMap` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`Homeomorph.symm_apply_apply` `homeomorph_comp`
`isCoveringMapOn` 📖	mathematical	`IsCoveringMap`	`IsCoveringMapOn` `Set.univ`	—	`isCoveringMap_iff_isCoveringMapOn_univ`
`isLocalHomeomorph` 📖	mathematical	`IsCoveringMap`	`IsLocalHomeomorph`	—	`isLocalHomeomorph_iff_isLocalHomeomorphOn_univ` `IsCoveringMapOn.isLocalHomeomorphOn` `isCoveringMapOn`
`isOpenMap` 📖	mathematical	`IsCoveringMap`	`IsOpenMap`	—	`IsLocalHomeomorph.isOpenMap` `isLocalHomeomorph`
`isQuotientMap` 📖	mathematical	`IsCoveringMap`	`Topology.IsQuotientMap`	—	`IsOpenMap.isQuotientMap` `isOpenMap` `continuous`
`isSeparatedMap` 📖	mathematical	`IsCoveringMap`	`IsSeparatedMap`	—	`IsEvenlyCovered.discreteTopology_fiber` `IsEvenlyCovered.mem_toTrivialization_baseSet` `ContinuousOn.isOpen_inter_preimage` `OpenPartialHomeomorph.continuousOn_toFun` `OpenPartialHomeomorph.open_source` `Continuous.isOpen_preimage` `continuous_snd` `isOpen_discrete` `Trivialization.mem_source` `Set.disjoint_left` `OpenPartialHomeomorph.injOn` `Trivialization.proj_toFun`
`mk` 📖	mathematical	`DiscreteTopology` `Set` `Set.instMembership` `Trivialization.baseSet`	`IsCoveringMap`	—	`isCoveringMap_iff_isCoveringMapOn_univ`
`mk'` 📖	mathematical	`DiscreteTopology`	`IsCoveringMap`	—	`isCoveringMap_iff_isCoveringMapOn_univ` `IsCoveringMapOn.mk'` `IsOpen.mem_nhds` `IsClosed.isOpen_compl` `Set.eq_empty_of_forall_notMem`
`of_discreteTopology` 📖	mathematical	—	`IsCoveringMap`	—	`instDiscreteTopologySubtype` `isOpen_discrete` `Unique.instSubsingleton` `Continuous.prodMk` `continuous_const` `continuous_id'` `Continuous.snd`
`of_isEmpty` 📖	mathematical	—	`IsCoveringMap`	—	`isCoveringMap_iff_isCoveringMapOn_univ` `IsCoveringMapOn.of_isEmpty`
`restrictPreimage` 📖	mathematical	`IsCoveringMap`	`Set.Elem` `Set.preimage` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrictPreimage`	—	`isCoveringMap_iff_isCoveringMapOn_univ` `IsCoveringMapOn.restrictPreimage`

IsCoveringMapOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_homeomorph` 📖	mathematical	`IsCoveringMapOn`	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`IsEvenlyCovered.to_isEvenlyCovered_preimage` `IsEvenlyCovered.comp_homeomorph`
`comp_homeomorph_iff` 📖	mathematical	—	`IsCoveringMapOn` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`Homeomorph.apply_symm_apply` `comp_homeomorph`
`continuousAt` 📖	mathematical	`IsCoveringMapOn` `Set` `Set.instMembership`	`ContinuousAt`	—	`IsEvenlyCovered.continuousAt`
`continuousOn` 📖	mathematical	`IsCoveringMapOn`	`ContinuousOn` `Set.preimage`	—	`continuousOn_of_forall_continuousAt` `continuousAt`
`homeomorph_comp` 📖	mathematical	`IsCoveringMapOn`	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Set.preimage` `Homeomorph.symm`	—	`IsEvenlyCovered.to_isEvenlyCovered_preimage` `IsEvenlyCovered.homeomorph_comp` `Homeomorph.apply_symm_apply`
`homeomorph_comp_iff` 📖	mathematical	—	`IsCoveringMapOn` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Set.preimage` `Homeomorph.symm`	—	`Homeomorph.symm_apply_apply` `Set.ext` `homeomorph_comp`
`isCoveringMap_restrictPreimage` 📖	mathematical	`IsCoveringMapOn`	`IsCoveringMap` `Set.Elem` `Set.preimage` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrictPreimage`	—	`isCoveringMap_iff_isCoveringMapOn_univ` `Subtype.coe_preimage_self` `restrictPreimage`
`isLocalHomeomorphOn` 📖	mathematical	`IsCoveringMapOn`	`IsLocalHomeomorphOn` `Set.preimage`	—	`IsEvenlyCovered.mem_toTrivialization_baseSet` `Trivialization.mem_source` `IsOpen.prod` `Trivialization.open_baseSet` `discreteTopology_iff_isOpen_singleton` `continuousOn_fst` `ContinuousOn.prodMk` `continuousOn_id'` `continuousOn_const` `OpenPartialHomeomorph.symm_symm` `Trivialization.proj_toFun` `IsEvenlyCovered.toTrivialization_apply`
`mk` 📖	mathematical	`DiscreteTopology` `Set` `Set.instMembership` `Trivialization.baseSet`	`IsCoveringMapOn`	—	`isEmpty_or_nonempty` `of_isEmpty` `mk'` `Trivialization.proj_symm_apply'`
`mk'` 📖	mathematical	`DiscreteTopology` `Set` `Filter` `Filter.instMembership` `nhds` `Set.instMembership` `Set.preimage` `Set.instEmptyCollection`	`IsCoveringMapOn`	—	`CanLift.prf` `Subtype.canLift` `IsEvenlyCovered.to_isEvenlyCovered_preimage` `IsEvenlyCovered.of_trivialization` `IsEvenlyCovered.of_preimage_eq_empty` `Empty.instIsEmpty`
`mono` 📖	—	`IsCoveringMapOn` `Set` `Set.instHasSubset`	—	—	—
`of_isCoveringMap_restrictPreimage` 📖	mathematical	`IsOpen` `Set.preimage` `IsCoveringMap` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrictPreimage`	`IsCoveringMapOn`	—	`IsEvenlyCovered.to_isEvenlyCovered_preimage` `IsEvenlyCovered.comp_subtypeVal` `IsEvenlyCovered.subtypeVal_comp`
`of_isCoveringMap_subtype` 📖	mathematical	`IsOpen` `Set` `Set.instMembership` `IsCoveringMap` `instTopologicalSpaceSubtype`	`IsCoveringMapOn`	—	`of_isCoveringMap_restrictPreimage` `IsCoveringMap.comp_homeomorph`
`of_isEmpty` 📖	mathematical	—	`IsCoveringMapOn`	—	`IsEvenlyCovered.to_isEvenlyCovered_preimage` `IsEvenlyCovered.of_preimage_eq_empty` `Empty.instIsEmpty` `Filter.univ_mem` `Set.eq_empty_of_isEmpty` `instIsEmptySubtype`
`of_openPartialHomeomorph` 📖	mathematical	`Continuous` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `OpenPartialHomeomorph.toFun'`	`IsCoveringMapOn`	—	`IsEvenlyCovered.of_openPartialHomeomorph`
`restrictPreimage` 📖	mathematical	`IsCoveringMapOn`	`Set.Elem` `Set.preimage` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Set.restrictPreimage`	—	`IsEvenlyCovered.to_isEvenlyCovered_preimage` `IsEvenlyCovered.restrictPreimage`

IsDiscrete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_openPartialHomeomorph` 📖	mathematical	`Set` `Set.instHasSubset` `Set.preimage` `Set.instSingletonSet` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `OpenPartialHomeomorph.toFun'`	`IsDiscrete`	—	`isDiscrete_iff_forall_exists_isOpen` `OpenPartialHomeomorph.open_source` `subset_antisymm` `Set.instAntisymmSubset` `OpenPartialHomeomorph.injOn` `Set.singleton_subset_iff`

IsEvenlyCovered

Definitions

Name	Category	Theorems
`fiberHomeomorph` 📖	CompOp	—
`toTrivialization` 📖	CompOp	2 math math: `toTrivialization_apply`, `mem_toTrivialization_baseSet`
`toTrivialization'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_homeomorph` 📖	mathematical	`IsEvenlyCovered`	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`IsOpen.preimage` `Homeomorph.continuous` `Set.preimage_comp` `Homeomorph.image_symm`
`comp_homeomorph_iff` 📖	mathematical	—	`IsEvenlyCovered` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`Homeomorph.apply_symm_apply` `comp_homeomorph`
`comp_subtypeVal` 📖	—	`IsOpen` `Set.preimage` `Set` `Set.instMembership` `IsEvenlyCovered` `Set.Elem` `instTopologicalSpaceSubtype`	—	—	`isEmpty_or_nonempty` `of_preimage_eq_empty` `IsOpen.mem_nhds` `IsOpen.inter` `Set.not_nonempty_iff_eq_empty` `Homeomorph.apply_symm_apply` `Set.mem_preimage` `Set.ext` `IsOpen.isOpenMap_subtype_val` `Topology.IsEmbedding.subtypeVal` `Homeomorph.symm_apply_eq`
`continuousAt` 📖	mathematical	`IsEvenlyCovered`	`ContinuousAt`	—	`Trivialization.continuousAt_proj` `Trivialization.mem_source` `mem_toTrivialization_baseSet`
`discreteTopology_fiber` 📖	mathematical	`IsEvenlyCovered`	`DiscreteTopology` `Set.Elem` `Set.preimage` `Set` `Set.instSingletonSet` `instTopologicalSpaceSubtype` `Set.instMembership`	—	`Homeomorph.discreteTopology`
`homeomorph_comp` 📖	mathematical	`IsEvenlyCovered`	`DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`Homeomorph.isOpen_image` `Homeomorph.preimage_image`
`homeomorph_comp_iff` 📖	mathematical	—	`IsEvenlyCovered` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	`Homeomorph.symm_apply_apply` `homeomorph_comp`
`mem_toTrivialization_baseSet` 📖	mathematical	`IsEvenlyCovered`	`Set` `Set.instMembership` `Trivialization.baseSet` `Set.Elem` `Set.preimage` `Set.instSingletonSet` `instTopologicalSpaceSubtype` `toTrivialization`	—	—
`of_fiber_homeomorph` 📖	—	`IsEvenlyCovered`	—	—	`Homeomorph.discreteTopology`
`of_openPartialHomeomorph` 📖	mathematical	`Continuous` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `OpenPartialHomeomorph.toFun'`	`IsEvenlyCovered` `Set.Elem` `Set.preimage` `Set.instSingletonSet` `instTopologicalSpaceSubtype`	—	`IsClosedMap.isEvenlyCovered_of_openPartialHomeomorph` `Continuous.isClosedMap` `IsCompact.finite` `IsClosed.isCompact` `IsClosed.preimage` `isClosed_singleton` `T2Space.t1Space` `IsDiscrete.of_openPartialHomeomorph` `subset_rfl` `Set.instReflSubset`
`of_preimage_eq_empty` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `Set.preimage` `Set.instEmptyCollection`	`IsEvenlyCovered`	—	`mem_nhds_iff` `Set.eq_empty_of_subset_empty` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.preimage_mono` `Eq.le` `Set.isEmpty_coe_sort` `Subsingleton.discreteTopology` `IsEmpty.instSubsingleton` `isOpen_empty` `Prod.isEmpty_right`
`of_trivialization` 📖	mathematical	`Set` `Set.instMembership` `Trivialization.baseSet`	`IsEvenlyCovered`	—	`Trivialization.open_baseSet` `OpenPartialHomeomorph.open_source` `Trivialization.source_eq` `Set.mem_preimage` `Trivialization.mem_source` `Trivialization.map_target` `Trivialization.target_eq` `Trivialization.symm_apply_mk_proj` `Trivialization.proj_symm_apply'` `Subtype.coe_eta` `Trivialization.apply_symm_apply'` `Topology.IsInducing.continuous_iff` `Topology.IsInducing.prodMap` `Topology.IsInducing.subtypeVal` `Topology.IsInducing.id` `Continuous.congr` `continuousOn_iff_continuous_restrict` `ContinuousOn.mono` `OpenPartialHomeomorph.continuousOn_toFun` `Eq.ge` `Trivialization.mk_proj_snd'` `ContinuousOn.comp_continuous` `OpenPartialHomeomorph.continuousOn_invFun` `Continuous.prodMap` `continuous_subtype_val` `continuous_id`
`restrictPreimage` 📖	mathematical	`Set` `Set.instMembership` `IsEvenlyCovered`	`Set.Elem` `Set.preimage` `instTopologicalSpaceSubtype` `Set.restrictPreimage`	—	`IsOpen.preimage` `continuous_subtype_val` `Homeomorph.apply_symm_apply` `Subtype.coe_eta` `Homeomorph.symm_apply_apply` `Continuous.prodMk` `Continuous.comp'` `Continuous.fst` `Homeomorph.continuous` `Continuous.snd` `continuous_id'`
`subtypeVal_comp` 📖	—	`IsOpen` `IsEvenlyCovered` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	—	`Set.ext` `Subtype.coe_eta` `IsOpen.isOpenMap_subtype_val` `Topology.IsEmbedding.subtypeVal`
`toTrivialization_apply` 📖	mathematical	`IsEvenlyCovered`	`Set.Elem` `Set.preimage` `Set` `Set.instSingletonSet` `Trivialization.toFun'` `instTopologicalSpaceSubtype` `Set.instMembership` `toTrivialization`	—	`Homeomorph.injective` `Subtype.coe_eta` `Homeomorph.apply_symm_apply`
`to_isEvenlyCovered_preimage` 📖	mathematical	`IsEvenlyCovered`	`Set.Elem` `Set.preimage` `Set` `Set.instSingletonSet` `instTopologicalSpaceSubtype` `Set.instMembership`	—	`of_fiber_homeomorph`

IsFiberBundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoveringMap` 📖	mathematical	`Set` `Set.instMembership` `Trivialization.baseSet`	`IsCoveringMap`	—	—

IsOpen

Definitions

Name	Category	Theorems
`trivializationDiscrete` 📖	CompOp	3 math math: `trivializationDiscrete_target`, `trivializationDiscrete_baseSet`, `trivializationDiscrete_source`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trivializationDiscrete_baseSet` 📖	mathematical	`IsOpen` `Set` `Set.instInter` `Set.preimage` `Set.InjOn` `Set.SurjOn` `Pairwise` `Function.onFun` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.instHasSubset` `Set.iUnion`	`Trivialization.baseSet` `trivializationDiscrete`	—	—
`trivializationDiscrete_source` 📖	mathematical	`IsOpen` `Set` `Set.instInter` `Set.preimage` `Set.InjOn` `Set.SurjOn` `Pairwise` `Function.onFun` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.instHasSubset` `Set.iUnion`	`PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `instTopologicalSpaceProd` `Trivialization.toOpenPartialHomeomorph` `trivializationDiscrete`	—	—
`trivializationDiscrete_target` 📖	mathematical	`IsOpen` `Set` `Set.instInter` `Set.preimage` `Set.InjOn` `Set.SurjOn` `Pairwise` `Function.onFun` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `Set.instHasSubset` `Set.iUnion`	`PartialEquiv.target` `OpenPartialHomeomorph.toPartialEquiv` `instTopologicalSpaceProd` `Trivialization.toOpenPartialHomeomorph` `trivializationDiscrete` `SProd.sprod` `Set.instSProd` `Set.univ`	—	—

(root)

Definitions

Name	Category	Theorems
`IsCoveringMap` 📖	MathDef	19 math math: `IsCoveringMap.comp_homeomorph_iff`, `Complex.isCoveringMap_exp`, `isAddQuotientCoveringMap_iff_isCoveringMap_and`, `isCoveringMap_iff_isCoveringMapOn_univ`, `IsFiberBundle.isCoveringMap`, `IsCoveringMap.of_discreteTopology`, `isCoveringMap_zpow`, `IsCoveringMapOn.isCoveringMap_restrictPreimage`, `isQuotientCoveringMap_iff_isCoveringMap_and`, `IsAddQuotientCoveringMap.isCoveringMap`, `IsCoveringMap.homeomorph_comp_iff`, `IsCoveringMap.mk'`, `FiberBundle.isCoveringMap`, `IsCoveringMap.of_isEmpty`, `isCoveringMap_npow`, `IsCoveringMap.mk`, `Circle.isCoveringMap_exp`, `AddCircle.isCoveringMap_coe`, `IsQuotientCoveringMap.isCoveringMap`
`IsCoveringMapOn` 📖	MathDef	21 math math: `IsCoveringMapOn.homeomorph_comp_iff`, `Polynomial.isCoveringMapOn_eval`, `IsCoveringMapOn.of_isEmpty`, `IsClosedMap.isCoveringMapOn_of_openPartialHomeomorph`, `isCoveringMap_iff_isCoveringMapOn_univ`, `IsCoveringMapOn.of_isCoveringMap_restrictPreimage`, `IsCoveringMapOn.of_openPartialHomeomorph`, `IsCoveringMapOn.comp_homeomorph_iff`, `Topology.IsQuotientMap.isCoveringMapOn_of_properlyDiscontinuousVAdd`, `IsCoveringMapOn.mk`, `isCoveringMapOn_npow`, `Complex.isCoveringMapOn_exp`, `Topology.IsQuotientMap.isCoveringMapOn_of_smul_disjoint`, `Topology.IsQuotientMap.isCoveringMapOn_of_properlyDiscontinuousSMul`, `IsCoveringMapOn.mk'`, `isCoveringMapOn_quotientMk_of_properlyDiscontinuousVAdd`, `isCoveringMapOn_quotientMk_of_properlyDiscontinuousSMul`, `IsCoveringMapOn.of_isCoveringMap_subtype`, `isCoveringMapOn_zpow`, `Topology.IsQuotientMap.isCoveringMapOn_of_vadd_disjoint`, `IsCoveringMap.isCoveringMapOn`
`IsEvenlyCovered` 📖	MathDef	6 math math: `IsClosedMap.isEvenlyCovered_of_openPartialHomeomorph`, `IsEvenlyCovered.of_preimage_eq_empty`, `IsEvenlyCovered.comp_homeomorph_iff`, `IsEvenlyCovered.of_trivialization`, `IsEvenlyCovered.of_openPartialHomeomorph`, `IsEvenlyCovered.homeomorph_comp_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoveringMap_iff_isCoveringMapOn_univ` 📖	mathematical	—	`IsCoveringMap` `IsCoveringMapOn` `Set.univ`	—	—

---

← Back to Index