Documentation Verification Report

IsLocalHomeomorph

📁 Source: Mathlib/Topology/IsLocalHomeomorph.lean

Statistics

Metric	Count
Definitions `IsLocalHomeomorph`, `toHomeomorphOfBijective`, `toHomeomorph_of_bijective`, `IsLocalHomeomorphOn`	4
Theorems `isLocalHomeomorph`, `isLocalHomeomorph`, `comap_discreteTopology`, `comp`, `continuous`, `discreteTopology_iff_of_surjective`, `discreteTopology_range_iff`, `isLocalHomeomorphOn`, `isLocallyInjective`, `isOpenEmbedding_of_comp`, `isOpenEmbedding_of_injective`, `isOpenMap`, `isTopologicalBasis`, `map_nhds_eq`, `mk`, `of_comp`, `isLocalHomeomorphOn`, `comp`, `continuousAt`, `continuousOn`, `discreteTopology_image_iff`, `discreteTopology_of_image`, `isDiscrete_image_iff`, `isDiscrete_of_image`, `map_nhds_eq`, `mk`, `mono`, `of_comp_left`, `of_comp_right`, `isLocalHomeomorph`, `isLocalHomeomorphOn_iff_isOpenEmbedding_restrict`, `isLocalHomeomorph_iff_isLocalHomeomorphOn_univ`, `isLocalHomeomorph_iff_isOpenEmbedding_restrict`	33
Total	37

Homeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalHomeomorph` 📖	mathematical	—	`IsLocalHomeomorph` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `instEquivLike`	—	—

IsLocalHomeomorph

Definitions

Name	Category	Theorems
`toHomeomorphOfBijective` 📖	CompOp	—
`toHomeomorph_of_bijective` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_discreteTopology` 📖	mathematical	`IsLocalHomeomorph`	`DiscreteTopology`	—	`Homeomorph.discreteTopology_iff` `IsLocalHomeomorphOn.discreteTopology_of_image` `isLocalHomeomorphOn` `instDiscreteTopologySubtype`
`comp` 📖	—	`IsLocalHomeomorph`	—	—	`isLocalHomeomorph_iff_isLocalHomeomorphOn_univ` `IsLocalHomeomorphOn.comp` `isLocalHomeomorphOn` `Set.mapsTo_univ`
`continuous` 📖	mathematical	`IsLocalHomeomorph`	`Continuous`	—	`continuousOn_univ` `IsLocalHomeomorphOn.continuousOn` `isLocalHomeomorphOn`
`discreteTopology_iff_of_surjective` 📖	mathematical	`IsLocalHomeomorph`	`DiscreteTopology`	—	`Homeomorph.discreteTopology_iff` `Function.Surjective.range_eq` `discreteTopology_range_iff`
`discreteTopology_range_iff` 📖	mathematical	`IsLocalHomeomorph`	`DiscreteTopology` `Set.Elem` `Set.range` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`Set.image_univ` `Homeomorph.discreteTopology_iff` `IsLocalHomeomorphOn.discreteTopology_image_iff` `isLocalHomeomorphOn` `isOpen_univ`
`isLocalHomeomorphOn` 📖	mathematical	`IsLocalHomeomorph`	`IsLocalHomeomorphOn`	—	—
`isLocallyInjective` 📖	mathematical	`IsLocalHomeomorph`	`IsLocallyInjective`	—	`OpenPartialHomeomorph.open_source` `OpenPartialHomeomorph.injOn`
`isOpenEmbedding_of_comp` 📖	—	`IsLocalHomeomorph` `Topology.IsOpenEmbedding` `Continuous`	—	—	`isOpenEmbedding_of_injective` `of_comp` `Topology.IsOpenEmbedding.isLocalHomeomorph` `Function.Injective.of_comp` `Topology.IsEmbedding.injective` `Topology.IsOpenEmbedding.toIsEmbedding`
`isOpenEmbedding_of_injective` 📖	mathematical	`IsLocalHomeomorph`	`Topology.IsOpenEmbedding`	—	`Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap` `continuous` `isOpenMap`
`isOpenMap` 📖	mathematical	`IsLocalHomeomorph`	`IsOpenMap`	—	`IsOpenMap.of_nhds_le` `ge_of_eq` `map_nhds_eq`
`isTopologicalBasis` 📖	mathematical	`IsLocalHomeomorph`	`TopologicalSpace.IsTopologicalBasis` `setOf` `Set` `IsOpen` `ContinuousMap` `Set.Elem` `instTopologicalSpaceSubtype` `Set.instMembership` `DFunLike.coe` `ContinuousMap.instFunLike` `Set.range`	—	`TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds` `Topology.IsOpenEmbedding.isOpen_range` `isOpenEmbedding_of_comp` `Topology.IsEmbedding.subtypeVal` `Subtype.range_val` `ContinuousMap.continuous` `OpenPartialHomeomorph.isOpen_inter_preimage` `continuousOn_iff_continuous_restrict` `ContinuousOn.mono` `OpenPartialHomeomorph.continuousOn_invFun` `OpenPartialHomeomorph.right_inv` `Set.range_restrict` `OpenPartialHomeomorph.symm_image_target_inter_eq` `Set.preimage_inter` `Set.inter_assoc` `Set.inter_eq_self_of_subset_left` `OpenPartialHomeomorph.source_preimage_target` `OpenPartialHomeomorph.source_inter_preimage_inv_preimage`
`map_nhds_eq` 📖	mathematical	`IsLocalHomeomorph`	`Filter.map` `nhds`	—	`IsLocalHomeomorphOn.map_nhds_eq` `isLocalHomeomorphOn` `Set.mem_univ`
`mk` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `Set.EqOn` `OpenPartialHomeomorph.toFun'`	`IsLocalHomeomorph`	—	`isLocalHomeomorph_iff_isLocalHomeomorphOn_univ`
`of_comp` 📖	—	`IsLocalHomeomorph` `Continuous`	—	—	`isLocalHomeomorph_iff_isLocalHomeomorphOn_univ` `IsLocalHomeomorphOn.of_comp_left` `isLocalHomeomorphOn` `Continuous.continuousAt`

IsLocalHomeomorph.Homeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalHomeomorph` 📖	mathematical	—	`IsLocalHomeomorph` `DFunLike.coe` `Homeomorph` `EquivLike.toFunLike` `Homeomorph.instEquivLike`	—	—

IsLocalHomeomorphOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`IsLocalHomeomorphOn` `Set.MapsTo`	—	—	—
`continuousAt` 📖	mathematical	`IsLocalHomeomorphOn` `Set` `Set.instMembership`	`ContinuousAt`	—	`Eq.le` `map_nhds_eq`
`continuousOn` 📖	mathematical	`IsLocalHomeomorphOn`	`ContinuousOn`	—	`continuousOn_of_forall_continuousAt` `continuousAt`
`discreteTopology_image_iff` 📖	mathematical	`IsLocalHomeomorphOn` `IsOpen`	`DiscreteTopology` `Set.Elem` `Set.image` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`discreteTopology_of_image` `OpenPartialHomeomorph.isOpen_image_of_subset_source` `Set.image_singleton` `IsOpen.isOpenMap_subtype_val` `Set.singleton_subset_iff` `Set.ext`
`discreteTopology_of_image` 📖	mathematical	`IsLocalHomeomorphOn`	`DiscreteTopology` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`discreteTopology_iff_isOpen_singleton` `isOpen_discrete` `ContinuousOn.isOpen_inter_preimage` `OpenPartialHomeomorph.continuousOn_toFun` `OpenPartialHomeomorph.open_source` `subset_antisymm` `Set.instAntisymmSubset` `OpenPartialHomeomorph.injOn` `Set.subset_singleton_iff` `Eq.subset` `Set.instReflSubset` `Eq.superset`
`isDiscrete_image_iff` 📖	mathematical	`IsLocalHomeomorphOn` `IsOpen`	`IsDiscrete` `Set.image`	—	`isDiscrete_of_image` `discreteTopology_image_iff` `IsDiscrete.to_subtype`
`isDiscrete_of_image` 📖	—	`IsLocalHomeomorphOn` `IsDiscrete` `Set.image`	—	—	`IsDiscrete.to_subtype` `discreteTopology_of_image`
`map_nhds_eq` 📖	mathematical	`IsLocalHomeomorphOn` `Set` `Set.instMembership`	`Filter.map` `nhds`	—	`OpenPartialHomeomorph.map_nhds_eq`
`mk` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `Set.EqOn` `OpenPartialHomeomorph.toFun'`	`IsLocalHomeomorphOn`	—	`PartialEquiv.map_source'` `PartialEquiv.map_target'` `PartialEquiv.left_inv'` `PartialEquiv.right_inv'` `OpenPartialHomeomorph.open_source` `OpenPartialHomeomorph.open_target` `continuousOn_congr` `OpenPartialHomeomorph.continuousOn_toFun` `OpenPartialHomeomorph.continuousOn_invFun`
`mono` 📖	—	`IsLocalHomeomorphOn` `Set` `Set.instHasSubset`	—	—	—
`of_comp_left` 📖	—	`IsLocalHomeomorphOn` `Set.image` `ContinuousAt`	—	—	`mem_interior_iff_mem_nhds` `ContinuousAt.preimage_mem_nhds` `IsOpen.mem_nhds` `OpenPartialHomeomorph.open_source` `OpenPartialHomeomorph.map_source` `interior_subset` `OpenPartialHomeomorph.eq_symm_apply`
`of_comp_right` 📖	mathematical	`IsLocalHomeomorphOn`	`Set.image`	—	`OpenPartialHomeomorph.map_source` `OpenPartialHomeomorph.left_inv` `OpenPartialHomeomorph.right_inv`

IsLocalHomeomorphOn.OpenPartialHomeomorph

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalHomeomorphOn` 📖	mathematical	—	`IsLocalHomeomorphOn` `OpenPartialHomeomorph.toFun'` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	—	—

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalHomeomorph` 📖	mathematical	`Topology.IsOpenEmbedding`	`IsLocalHomeomorph`	—	`isLocalHomeomorph_iff_isOpenEmbedding_restrict` `Filter.univ_mem` `comp` `Homeomorph.isOpenEmbedding`

(root)

Definitions

Name	Category	Theorems
`IsLocalHomeomorph` 📖	MathDef	10 math math: `Topology.IsOpenEmbedding.isLocalHomeomorph`, `isLocalHomeomorph_iff_isLocalHomeomorphOn_univ`, `IsLocalHomeomorph.Homeomorph.isLocalHomeomorph`, `IsLocalDiffeomorph.isLocalHomeomorph`, `AddCircle.isLocalHomeomorph_coe`, `Homeomorph.isLocalHomeomorph`, `isLocalHomeomorph_iff_isOpenEmbedding_restrict`, `isLocalHomeomorph_circleExp`, `IsCoveringMap.isLocalHomeomorph`, `IsLocalHomeomorph.mk`
`IsLocalHomeomorphOn` 📖	MathDef	7 math math: `IsLocalHomeomorphOn.mk`, `isLocalHomeomorph_iff_isLocalHomeomorphOn_univ`, `IsLocalHomeomorphOn.OpenPartialHomeomorph.isLocalHomeomorphOn`, `IsLocalHomeomorph.isLocalHomeomorphOn`, `isLocalHomeomorphOn_iff_isOpenEmbedding_restrict`, `IsCoveringMapOn.isLocalHomeomorphOn`, `IsLocalDiffeomorphOn.isLocalHomeomorphOn`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isLocalHomeomorphOn_iff_isOpenEmbedding_restrict` 📖	mathematical	—	`IsLocalHomeomorphOn` `Set` `Filter` `Filter.instMembership` `nhds` `Topology.IsOpenEmbedding` `Set.Elem` `instTopologicalSpaceSubtype` `Set.instMembership` `Set.restrict`	—	`IsOpen.mem_nhds` `OpenPartialHomeomorph.open_source` `OpenPartialHomeomorph.isOpenEmbedding_restrict` `Topology.IsOpenEmbedding.comp` `interior_subset` `Topology.IsEmbedding.inclusion` `Set.range_inclusion` `isOpen_induced` `isOpen_interior` `Topology.isOpenEmbedding_iff_continuous_injective_isOpenMap` `Set.injOn_iff_injective` `continuousOn_iff_continuous_restrict` `mem_interior_iff_mem_nhds`
`isLocalHomeomorph_iff_isLocalHomeomorphOn_univ` 📖	mathematical	—	`IsLocalHomeomorph` `IsLocalHomeomorphOn` `Set.univ`	—	—
`isLocalHomeomorph_iff_isOpenEmbedding_restrict` 📖	mathematical	—	`IsLocalHomeomorph` `Set` `Filter` `Filter.instMembership` `nhds` `Topology.IsOpenEmbedding` `Set.Elem` `instTopologicalSpaceSubtype` `Set.instMembership` `Set.restrict`	—	`Set.mem_univ`

---

← Back to Index