Basic

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

Statistics

Metric	Count
Definitions	0
Theorems `preimage`, `isEmbedding_induced`, `isEmbedding`, `closure_image_eq_of_continuous`, `closure_image_subset`, `comap_nhdsSet_eq`, `comap_nhdsSet_le`, `comap_nhds_eq`, `comap_nhds_le`, `comp`, `eventually_nhds_fiber`, `frequently_nhds_fiber`, `id`, `isClosed_range`, `isQuotientMap`, `lift'_closure_map_eq`, `mapClusterPt_iff_lift'_closure`, `of_comp_surjective`, `of_inverse`, `of_nonempty`, `clusterPt_comap`, `comp`, `id`, `image_interior_subset`, `image_mem_nhds`, `interior_preimage_subset_preimage_interior`, `isOpen_range`, `isQuotientMap`, `map_nhdsSet_eq`, `map_nhds_eq`, `mapsTo_interior`, `nhds_le`, `of_inverse`, `of_isEmpty`, `of_nhds_le`, `of_sections`, `preimage_closure_eq_closure_preimage`, `preimage_closure_subset_closure_preimage`, `preimage_frontier_eq_frontier_preimage`, `preimage_frontier_subset_frontier_preimage`, `preimage_interior_eq_interior_preimage`, `range_mem_nhds`, `closure_image_eq`, `comp`, `continuous`, `id`, `isClosedEmbedding_iff_continuous_injective_isClosedMap`, `isClosedMap`, `isClosed_iff_image_isClosed`, `isClosed_iff_preimage_isClosed`, `isEmbedding`, `isInducing`, `of_comp`, `of_comp_iff`, `of_continuous_injective_isClosedMap`, `of_isEmbedding_isClosedMap`, `tendsto_nhds_iff`, `closure_eq_preimage_closure_image`, `comp`, `continuous`, `continuous_iff`, `discreteTopology`, `id`, `induced`, `isInducing`, `isOpenEmbedding_of_surjective`, `map_nhds_eq`, `map_nhds_of_mem`, `mk'`, `of_comp`, `of_comp_iff`, `of_leftInverse`, `of_subsingleton`, `tendsto_nhds_iff`, `basis_nhds`, `closure_eq_preimage_closure_image`, `comp`, `continuous`, `continuousAt_iff`, `continuousAt_iff'`, `continuous_iff`, `dense_iff`, `id`, `image_mem_nhdsWithin`, `indiscreteTopology`, `induced`, `isClosedMap`, `isClosed_iff`, `isClosed_iff'`, `isClosed_preimage`, `isOpenMap`, `isOpen_iff`, `mapClusterPt_iff`, `map_nhds_eq`, `map_nhds_of_mem`, `nhdsSet_eq_comap`, `nhds_eq_comap`, `nontrivialTopology`, `of_comp`, `of_comp_iff`, `of_subsingleton`, `setOf_isOpen`, `tendsto_nhds_iff`, `comp`, `continuous`, `continuousAt_iff`, `id`, `image_mem_nhds`, `isEmbedding`, `isInducing`, `isOpenMap`, `isOpenMap_iff`, `isOpen_iff_image_isOpen`, `isOpen_iff_preimage_isOpen`, `map_nhds_eq`, `of_comp`, `of_comp_iff`, `of_continuous_injective_isOpenMap`, `of_isEmbedding`, `of_isEmbedding_isOpenMap`, `of_isEmpty`, `tendsto_nhds_iff`, `tendsto_nhds_iff'`, `comp`, `continuous`, `continuous_iff`, `id`, `isClosed_preimage`, `isOpen_preimage`, `of_comp`, `of_comp_isQuotientMap`, `of_comp_of_eq_coinduced`, `of_inverse`, `isInducing_iff_nhds`, `isOpenEmbedding_iff_continuous_injective_isOpenMap`, `isOpenEmbedding_iff_isEmbedding_isOpenMap`, `isQuotientMap_iff`, `isQuotientMap_iff_isClosed`, `isClosedMap_iff_closure_image`, `isClosedMap_iff_clusterPt`, `isClosedMap_iff_comap_nhdsSet_le`, `isClosedMap_iff_comap_nhds_le`, `isClosedMap_iff_kernImage`, `isClosedMap_iff_kernImage_interior`, `isOpenMap_iff_closure_kernImage`, `isOpenMap_iff_clusterPt_comap`, `isOpenMap_iff_image_interior`, `isOpenMap_iff_interior`, `isOpenMap_iff_kernImage`, `isOpenMap_iff_nhds_le`	150
Total	150

Dense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`preimage` 📖	mathematical	`Dense` `IsOpenMap`	`Set.preimage`	—	`IsOpenMap.preimage_closure_subset_closure_preimage`

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEmbedding_induced` 📖	mathematical	—	`Topology.IsEmbedding` `TopologicalSpace.induced`	—	`Topology.IsEmbedding.induced`

Function.LeftInverse

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEmbedding` 📖	mathematical	`Continuous`	`Topology.IsEmbedding`	—	`Topology.IsEmbedding.of_leftInverse`

IsClosedMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_image_eq_of_continuous` 📖	mathematical	`IsClosedMap` `Continuous`	`closure` `Set.image`	—	`subset_antisymm` `Set.instAntisymmSubset` `closure_image_subset` `image_closure_subset_closure_image`
`closure_image_subset` 📖	mathematical	`IsClosedMap`	`Set` `Set.instHasSubset` `closure` `Set.image`	—	`closure_minimal` `Set.image_mono` `subset_closure` `isClosed_closure`
`comap_nhdsSet_eq` 📖	mathematical	`IsClosedMap` `Continuous`	`Filter.comap` `nhdsSet` `Set.preimage`	—	`le_antisymm` `isClosedMap_iff_comap_nhdsSet_le` `nhdsSet_le` `LE.le.trans` `Filter.Tendsto.le_comap` `Continuous.tendsto` `Filter.comap_mono` `nhds_le_nhdsSet`
`comap_nhdsSet_le` 📖	mathematical	`IsClosedMap`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.comap` `nhdsSet` `Set.preimage`	—	`isClosedMap_iff_comap_nhdsSet_le`
`comap_nhds_eq` 📖	mathematical	`IsClosedMap` `Continuous`	`Filter.comap` `nhds` `nhdsSet` `Set.preimage` `Set` `Set.instSingletonSet`	—	`le_antisymm` `isClosedMap_iff_comap_nhds_le` `nhdsSet_le` `Filter.Tendsto.le_comap` `Continuous.tendsto`
`comap_nhds_le` 📖	mathematical	`IsClosedMap`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.comap` `nhds` `nhdsSet` `Set.preimage` `Set` `Set.instSingletonSet`	—	`isClosedMap_iff_comap_nhds_le`
`comp` 📖	—	`IsClosedMap`	—	—	`Set.image_comp`
`eventually_nhds_fiber` 📖	—	`IsClosedMap` `Filter.Eventually` `nhds`	—	—	`Filter.Eventually.filter_mono` `comap_nhds_le` `eventually_nhdsSet_iff_forall` `Filter.eventually_comap`
`frequently_nhds_fiber` 📖	—	`IsClosedMap` `Filter.Frequently` `Set` `Set.instMembership` `Set.preimage` `Set.instSingletonSet` `nhds`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `eventually_nhds_fiber`
`id` 📖	mathematical	—	`IsClosedMap`	—	`Set.image_id`
`isClosed_range` 📖	mathematical	`IsClosedMap`	`IsClosed` `Set.range`	—	`isClosed_univ` `Set.image_univ`
`isQuotientMap` 📖	mathematical	`IsClosedMap` `Continuous`	`Topology.IsQuotientMap`	—	`Topology.isQuotientMap_iff_isClosed` `IsClosed.preimage` `Function.Surjective.image_preimage`
`lift'_closure_map_eq` 📖	mathematical	`IsClosedMap` `Continuous`	`Filter.lift'` `Filter.map` `closure`	—	`Filter.map_lift'_eq2` `monotone_closure` `Filter.map_lift'_eq` `closure_image_eq_of_continuous`
`mapClusterPt_iff_lift'_closure` 📖	mathematical	`IsClosedMap` `Continuous`	`MapClusterPt` `Filter.NeBot` `Filter` `Filter.instInf` `Filter.lift'` `closure` `Filter.principal` `Set.preimage` `Set` `Set.instSingletonSet`	—	`MapClusterPt.eq_1` `clusterPt_iff_lift'_closure'` `lift'_closure_map_eq` `Filter.comap_principal` `Filter.map_neBot_iff` `Filter.push_pull` `Filter.principal_singleton`
`of_comp_surjective` 📖	—	`Continuous` `IsClosedMap`	—	—	`Set.image_preimage_eq` `Set.image_comp` `IsClosed.preimage`
`of_inverse` 📖	mathematical	`Continuous`	`IsClosedMap`	—	`Set.image_eq_preimage_of_inverse` `IsClosed.preimage`
`of_nonempty` 📖	mathematical	`IsClosed` `Set.image`	`IsClosedMap`	—	`Set.eq_empty_or_nonempty` `Set.image_empty`

IsOpenMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clusterPt_comap` 📖	mathematical	`IsOpenMap`	`ClusterPt` `Filter.comap`	—	`ClusterPt.eq_1` `Filter.map_neBot_iff` `Filter.push_pull` `Filter.NeBot.mono` `ClusterPt.neBot` `inf_le_inf_right` `nhds_le`
`comp` 📖	—	`IsOpenMap`	—	—	`Set.image_comp`
`id` 📖	mathematical	—	`IsOpenMap`	—	`Set.image_id`
`image_interior_subset` 📖	mathematical	`IsOpenMap`	`Set` `Set.instHasSubset` `Set.image` `interior`	—	`Set.MapsTo.image_subset` `mapsTo_interior` `Set.mapsTo_image`
`image_mem_nhds` 📖	mathematical	`IsOpenMap` `Set` `Filter` `Filter.instMembership` `nhds`	`Set.image`	—	`mem_nhds_iff` `Filter.mem_of_superset` `IsOpen.mem_nhds` `Set.mem_image_of_mem` `Set.image_mono`
`interior_preimage_subset_preimage_interior` 📖	mathematical	`IsOpenMap`	`Set` `Set.instHasSubset` `interior` `Set.preimage`	—	`mapsTo_interior` `Set.mapsTo_preimage`
`isOpen_range` 📖	mathematical	`IsOpenMap`	`IsOpen` `Set.range`	—	`Set.image_univ` `isOpen_univ`
`isQuotientMap` 📖	mathematical	`IsOpenMap` `Continuous`	`Topology.IsQuotientMap`	—	`Topology.isQuotientMap_iff` `IsOpen.preimage` `Function.Surjective.image_preimage`
`map_nhdsSet_eq` 📖	mathematical	`IsOpenMap` `Continuous`	`Filter.map` `nhdsSet` `Set.image`	—	`Set.biUnion_of_singleton` `Set.image_iUnion` `nhdsSet_iUnion` `Filter.map_iSup` `iSup_congr_Prop` `Set.image_singleton` `nhdsSet_singleton` `map_nhds_eq` `Continuous.continuousAt`
`map_nhds_eq` 📖	mathematical	`IsOpenMap` `ContinuousAt`	`Filter.map` `nhds`	—	`le_antisymm` `nhds_le`
`mapsTo_interior` 📖	mathematical	`IsOpenMap` `Set.MapsTo`	`interior`	—	`Set.mapsTo_iff_image_subset` `interior_maximal` `Set.MapsTo.image_subset` `Set.MapsTo.mono` `interior_subset` `Set.Subset.rfl` `isOpen_interior`
`nhds_le` 📖	mathematical	`IsOpenMap`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds` `Filter.map`	—	`Filter.le_map` `image_mem_nhds`
`of_inverse` 📖	mathematical	`Continuous`	`IsOpenMap`	—	`of_sections` `Continuous.continuousAt`
`of_isEmpty` 📖	mathematical	—	`IsOpenMap`	—	`of_nhds_le`
`of_nhds_le` 📖	mathematical	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds` `Filter.map`	`IsOpenMap`	—	`isOpen_iff_mem_nhds` `Filter.image_mem_map` `IsOpen.mem_nhds`
`of_sections` 📖	mathematical	`ContinuousAt`	`IsOpenMap`	—	`of_nhds_le` `Filter.map_map` `Function.RightInverse.comp_eq_id` `Filter.map_id` `Filter.map_mono`
`preimage_closure_eq_closure_preimage` 📖	mathematical	`IsOpenMap` `Continuous`	`Set.preimage` `closure`	—	`HasSubset.Subset.antisymm` `Set.instAntisymmSubset` `preimage_closure_subset_closure_preimage` `Continuous.closure_preimage_subset`
`preimage_closure_subset_closure_preimage` 📖	mathematical	`IsOpenMap`	`Set` `Set.instHasSubset` `Set.preimage` `closure`	—	`Set.compl_subset_compl` `interior_preimage_subset_preimage_interior`
`preimage_frontier_eq_frontier_preimage` 📖	mathematical	`IsOpenMap` `Continuous`	`Set.preimage` `frontier`	—	`frontier_eq_closure_inter_closure` `preimage_closure_eq_closure_preimage`
`preimage_frontier_subset_frontier_preimage` 📖	mathematical	`IsOpenMap`	`Set` `Set.instHasSubset` `Set.preimage` `frontier`	—	`frontier_eq_closure_inter_closure` `Set.inter_subset_inter` `preimage_closure_subset_closure_preimage`
`preimage_interior_eq_interior_preimage` 📖	mathematical	`IsOpenMap` `Continuous`	`Set.preimage` `interior`	—	`Set.Subset.antisymm` `preimage_interior_subset_interior_preimage` `interior_preimage_subset_preimage_interior`
`range_mem_nhds` 📖	mathematical	`IsOpenMap`	`Set` `Filter` `Filter.instMembership` `nhds` `Set.range`	—	`IsOpen.mem_nhds` `isOpen_range` `Set.mem_range_self`

Topology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isInducing_iff_nhds` 📖	mathematical	—	`IsInducing` `nhds` `Filter.comap`	—	`isInducing_iff` `induced_iff_nhds_eq`
`isOpenEmbedding_iff_continuous_injective_isOpenMap` 📖	mathematical	—	`IsOpenEmbedding` `Continuous` `IsOpenMap`	—	`IsOpenEmbedding.continuous` `IsEmbedding.injective` `IsOpenEmbedding.toIsEmbedding` `IsOpenEmbedding.isOpenMap` `IsOpenEmbedding.of_continuous_injective_isOpenMap`
`isOpenEmbedding_iff_isEmbedding_isOpenMap` 📖	mathematical	—	`IsOpenEmbedding` `IsEmbedding` `IsOpenMap`	—	`IsOpenEmbedding.toIsEmbedding` `IsOpenEmbedding.isOpenMap` `IsOpenEmbedding.of_isEmbedding_isOpenMap`
`isQuotientMap_iff` 📖	mathematical	—	`IsQuotientMap` `IsOpen` `Set.preimage`	—	`isQuotientMap_iff'` `TopologicalSpace.ext_iff`
`isQuotientMap_iff_isClosed` 📖	mathematical	—	`IsQuotientMap` `IsClosed` `Set.preimage`	—	`isQuotientMap_iff` `Iff.and` `Function.Surjective.forall` `compl_surjective`

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_image_eq` 📖	mathematical	`Topology.IsClosedEmbedding`	`closure` `Set.image`	—	`IsClosedMap.closure_image_eq_of_continuous` `isClosedMap` `continuous`
`comp` 📖	—	`Topology.IsClosedEmbedding`	—	—	`Topology.IsEmbedding.comp` `isEmbedding` `IsClosedMap.isClosed_range` `IsClosedMap.comp` `isClosedMap`
`continuous` 📖	mathematical	`Topology.IsClosedEmbedding`	`Continuous`	—	`Topology.IsEmbedding.continuous` `isEmbedding`
`id` 📖	mathematical	—	`Topology.IsClosedEmbedding`	—	`Topology.IsEmbedding.id` `IsClosedMap.isClosed_range` `IsClosedMap.id`
`isClosedEmbedding_iff_continuous_injective_isClosedMap` 📖	mathematical	—	`Topology.IsClosedEmbedding` `Continuous` `IsClosedMap`	—	`continuous` `Topology.IsEmbedding.injective` `toIsEmbedding` `isClosedMap` `of_continuous_injective_isClosedMap`
`isClosedMap` 📖	mathematical	`Topology.IsClosedEmbedding`	`IsClosedMap`	—	`Topology.IsInducing.isClosedMap` `Topology.IsEmbedding.isInducing` `isEmbedding` `isClosed_range`
`isClosed_iff_image_isClosed` 📖	mathematical	`Topology.IsClosedEmbedding`	`IsClosed` `Set.image`	—	`isClosedMap` `Set.preimage_image_eq` `Topology.IsEmbedding.injective` `toIsEmbedding` `IsClosed.preimage` `continuous`
`isClosed_iff_preimage_isClosed` 📖	mathematical	`Topology.IsClosedEmbedding` `Set` `Set.instHasSubset` `Set.range`	`IsClosed` `Set.preimage`	—	`isClosed_iff_image_isClosed` `Set.image_preimage_eq_of_subset`
`isEmbedding` 📖	mathematical	`Topology.IsClosedEmbedding`	`Topology.IsEmbedding`	—	`toIsEmbedding`
`isInducing` 📖	mathematical	`Topology.IsClosedEmbedding`	`Topology.IsInducing`	—	`Topology.IsEmbedding.isInducing` `isEmbedding`
`of_comp` 📖	—	`Topology.IsEmbedding` `Topology.IsClosedEmbedding`	—	—	`Topology.IsEmbedding.of_comp_iff` `isEmbedding` `Set.range_comp` `Function.Injective.preimage_image` `Topology.IsEmbedding.injective` `Topology.IsInducing.isClosed_preimage` `Topology.IsEmbedding.toIsInducing` `isClosed_range`
`of_comp_iff` 📖	—	`Topology.IsClosedEmbedding`	—	—	`Topology.IsEmbedding.of_comp_iff` `isEmbedding` `Set.range_comp` `isClosed_iff_image_isClosed`
`of_continuous_injective_isClosedMap` 📖	mathematical	`Continuous` `IsClosedMap`	`Topology.IsClosedEmbedding`	—	`of_isEmbedding_isClosedMap` `LE.le.antisymm` `Continuous.le_induced` `IsClosed.isOpen_compl` `IsOpen.isClosed_compl` `Set.preimage_compl` `Set.preimage_image_eq` `compl_compl`
`of_isEmbedding_isClosedMap` 📖	mathematical	`Topology.IsEmbedding` `IsClosedMap`	`Topology.IsClosedEmbedding`	—	`isClosed_univ` `Set.image_univ`
`tendsto_nhds_iff` 📖	mathematical	`Topology.IsClosedEmbedding`	`Filter.Tendsto` `nhds`	—	`Topology.IsEmbedding.tendsto_nhds_iff` `isEmbedding`

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_eq_preimage_closure_image` 📖	mathematical	`Topology.IsEmbedding`	`closure` `Set.preimage` `Set.image`	—	`Topology.IsInducing.closure_eq_preimage_closure_image` `toIsInducing`
`comp` 📖	—	`Topology.IsEmbedding`	—	—	`Topology.IsInducing.comp` `isInducing` `injective`
`continuous` 📖	mathematical	`Topology.IsEmbedding`	`Continuous`	—	`Topology.IsInducing.continuous` `isInducing`
`continuous_iff` 📖	mathematical	`Topology.IsEmbedding`	`Continuous`	—	`Topology.IsInducing.continuous_iff` `isInducing`
`discreteTopology` 📖	mathematical	`Topology.IsEmbedding`	`DiscreteTopology`	—	`DiscreteTopology.of_continuous_injective` `continuous` `injective`
`id` 📖	mathematical	—	`Topology.IsEmbedding`	—	`Topology.IsInducing.id`
`induced` 📖	mathematical	—	`Topology.IsEmbedding` `TopologicalSpace.induced`	—	`Topology.IsInducing.induced`
`isInducing` 📖	mathematical	`Topology.IsEmbedding`	`Topology.IsInducing`	—	`toIsInducing`
`isOpenEmbedding_of_surjective` 📖	mathematical	`Topology.IsEmbedding`	`Topology.IsOpenEmbedding`	—	`isOpen_univ` `Function.Surjective.range_eq`
`map_nhds_eq` 📖	mathematical	`Topology.IsEmbedding`	`Filter.map` `nhds` `nhdsWithin` `Set.range`	—	`Topology.IsInducing.map_nhds_eq` `toIsInducing`
`map_nhds_of_mem` 📖	mathematical	`Topology.IsEmbedding` `Set` `Filter` `Filter.instMembership` `nhds` `Set.range`	`Filter.map`	—	`Topology.IsInducing.map_nhds_of_mem` `toIsInducing`
`mk'` 📖	mathematical	`Filter.comap` `nhds`	`Topology.IsEmbedding`	—	`Topology.isInducing_iff_nhds`
`of_comp` 📖	—	`Continuous` `Topology.IsEmbedding`	—	—	`Topology.IsInducing.of_comp` `isInducing` `Function.Injective.of_comp` `injective`
`of_comp_iff` 📖	—	`Topology.IsEmbedding`	—	—	`Topology.IsInducing.of_comp_iff` `isInducing` `Function.Injective.of_comp_iff` `injective`
`of_leftInverse` 📖	mathematical	`Continuous`	`Topology.IsEmbedding`	—	`of_comp` `id` `Function.LeftInverse.comp_eq_id`
`of_subsingleton` 📖	mathematical	—	`Topology.IsEmbedding`	—	`Topology.IsInducing.of_subsingleton` `Function.injective_of_subsingleton`
`tendsto_nhds_iff` 📖	mathematical	`Topology.IsEmbedding`	`Filter.Tendsto` `nhds`	—	`Topology.IsInducing.tendsto_nhds_iff` `isInducing`

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basis_nhds` 📖	mathematical	`Topology.IsInducing` `Filter.HasBasis` `nhds`	`Set` `Set.preimage`	—	`Filter.HasBasis.comap` `nhds_eq_comap`
`closure_eq_preimage_closure_image` 📖	mathematical	`Topology.IsInducing`	`closure` `Set.preimage` `Set.image`	—	`Set.ext` `Set.mem_preimage` `closure_induced` `eq_induced`
`comp` 📖	—	`Topology.IsInducing`	—	—	`eq_induced` `induced_compose`
`continuous` 📖	mathematical	`Topology.IsInducing`	`Continuous`	—	`continuous_iff` `continuous_id`
`continuousAt_iff` 📖	mathematical	`Topology.IsInducing`	`ContinuousAt`	—	`tendsto_nhds_iff`
`continuousAt_iff'` 📖	mathematical	`Topology.IsInducing` `Set` `Filter` `Filter.instMembership` `nhds` `Set.range`	`ContinuousAt`	—	`map_nhds_of_mem` `Filter.map_map`
`continuous_iff` 📖	mathematical	`Topology.IsInducing`	`Continuous`	—	`continuousAt_iff`
`dense_iff` 📖	mathematical	`Topology.IsInducing`	`Dense` `Set` `Set.instMembership` `closure` `Set.image`	—	`closure_eq_preimage_closure_image`
`id` 📖	mathematical	—	`Topology.IsInducing`	—	`induced_id`
`image_mem_nhdsWithin` 📖	mathematical	`Topology.IsInducing` `Set` `Filter` `Filter.instMembership` `nhds`	`nhdsWithin` `Set.range` `Set.image`	—	`Filter.image_mem_map` `map_nhds_eq`
`indiscreteTopology` 📖	mathematical	`Topology.IsInducing`	`IndiscreteTopology`	—	`IndiscreteTopology.eq_top` `eq_induced` `induced_top`
`induced` 📖	mathematical	—	`Topology.IsInducing` `TopologicalSpace.induced`	—	—
`isClosedMap` 📖	mathematical	`Topology.IsInducing`	`IsClosedMap`	—	`isClosed_iff` `Set.image_preimage_eq_inter_range` `IsClosed.inter`
`isClosed_iff` 📖	mathematical	`Topology.IsInducing`	`IsClosed` `Set.preimage`	—	`eq_induced` `isClosed_induced_iff`
`isClosed_iff'` 📖	mathematical	`Topology.IsInducing`	`IsClosed` `Set` `Set.instMembership`	—	`eq_induced` `isClosed_induced_iff'`
`isClosed_preimage` 📖	mathematical	`Topology.IsInducing`	`IsClosed` `Set.preimage`	—	`isClosed_iff`
`isOpenMap` 📖	mathematical	`Topology.IsInducing` `IsOpen` `Set.range`	`IsOpenMap`	—	`IsOpenMap.of_nhds_le` `Eq.ge` `map_nhds_of_mem` `IsOpen.mem_nhds` `Set.mem_range_self`
`isOpen_iff` 📖	mathematical	`Topology.IsInducing`	`IsOpen` `Set.preimage`	—	`eq_induced` `isOpen_induced_iff`
`mapClusterPt_iff` 📖	mathematical	`Topology.IsInducing`	`MapClusterPt` `ClusterPt`	—	`Filter.push_pull'` `nhds_eq_comap` `Filter.map_neBot_iff`
`map_nhds_eq` 📖	mathematical	`Topology.IsInducing`	`Filter.map` `nhds` `nhdsWithin` `Set.range`	—	`map_nhds_induced_eq` `eq_induced`
`map_nhds_of_mem` 📖	mathematical	`Topology.IsInducing` `Set` `Filter` `Filter.instMembership` `nhds` `Set.range`	`Filter.map`	—	`map_nhds_induced_of_mem` `eq_induced`
`nhdsSet_eq_comap` 📖	mathematical	`Topology.IsInducing`	`nhdsSet` `Filter.comap` `Set.image`	—	`Set.image_congr` `nhds_eq_comap` `sSup_image` `iSup_image` `Filter.comap_iSup`
`nhds_eq_comap` 📖	mathematical	`Topology.IsInducing`	`nhds` `Filter.comap`	—	`Topology.isInducing_iff_nhds`
`nontrivialTopology` 📖	mathematical	`Topology.IsInducing`	`NontrivialTopology`	—	`not_imp_not` `indiscreteTopology`
`of_comp` 📖	—	`Continuous` `Topology.IsInducing`	—	—	`le_antisymm` `Continuous.le_induced` `eq_induced` `induced_compose` `le_imp_le_of_le_of_le` `le_refl` `induced_mono`
`of_comp_iff` 📖	—	`Topology.IsInducing`	—	—	`Topology.isInducing_iff` `eq_induced` `induced_compose` `comp`
`of_subsingleton` 📖	mathematical	—	`Topology.IsInducing`	—	`Unique.instSubsingleton`
`setOf_isOpen` 📖	mathematical	`Topology.IsInducing`	`setOf` `Set` `IsOpen` `Set.image` `Set.preimage`	—	`Set.ext` `isOpen_iff`
`tendsto_nhds_iff` 📖	mathematical	`Topology.IsInducing`	`Filter.Tendsto` `nhds`	—	`nhds_eq_comap` `Filter.tendsto_comap_iff`

Topology.IsOpenEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`Topology.IsOpenEmbedding`	—	—	`Topology.IsEmbedding.comp` `toIsEmbedding` `IsOpenMap.isOpen_range` `IsOpenMap.comp` `isOpenMap`
`continuous` 📖	mathematical	`Topology.IsOpenEmbedding`	`Continuous`	—	`Topology.IsEmbedding.continuous` `isEmbedding`
`continuousAt_iff` 📖	mathematical	`Topology.IsOpenEmbedding`	`ContinuousAt`	—	`tendsto_nhds_iff'`
`id` 📖	mathematical	—	`Topology.IsOpenEmbedding`	—	`Topology.IsEmbedding.id` `IsOpenMap.isOpen_range` `IsOpenMap.id`
`image_mem_nhds` 📖	mathematical	`Topology.IsOpenEmbedding`	`Set` `Filter` `Filter.instMembership` `nhds` `Set.image`	—	`map_nhds_eq` `Filter.mem_map` `Set.preimage_image_eq` `Topology.IsEmbedding.injective` `toIsEmbedding`
`isEmbedding` 📖	mathematical	`Topology.IsOpenEmbedding`	`Topology.IsEmbedding`	—	`toIsEmbedding`
`isInducing` 📖	mathematical	`Topology.IsOpenEmbedding`	`Topology.IsInducing`	—	`Topology.IsEmbedding.isInducing` `isEmbedding`
`isOpenMap` 📖	mathematical	`Topology.IsOpenEmbedding`	`IsOpenMap`	—	`Topology.IsInducing.isOpenMap` `Topology.IsEmbedding.isInducing` `isEmbedding` `isOpen_range`
`isOpenMap_iff` 📖	mathematical	`Topology.IsOpenEmbedding`	`IsOpenMap`	—	`map_nhds_eq` `Filter.map_le_map_iff` `Topology.IsEmbedding.injective` `toIsEmbedding`
`isOpen_iff_image_isOpen` 📖	mathematical	`Topology.IsOpenEmbedding`	`IsOpen` `Set.image`	—	`isOpenMap` `Set.preimage_image_eq` `Topology.IsEmbedding.injective` `toIsEmbedding` `IsOpen.preimage` `Topology.IsEmbedding.continuous` `isEmbedding`
`isOpen_iff_preimage_isOpen` 📖	mathematical	`Topology.IsOpenEmbedding` `Set` `Set.instHasSubset` `Set.range`	`IsOpen` `Set.preimage`	—	`isOpen_iff_image_isOpen` `Set.image_preimage_eq_inter_range` `Set.inter_eq_self_of_subset_left`
`map_nhds_eq` 📖	mathematical	`Topology.IsOpenEmbedding`	`Filter.map` `nhds`	—	`Topology.IsEmbedding.map_nhds_of_mem` `isEmbedding` `IsOpen.mem_nhds` `isOpen_range` `Set.mem_range_self`
`of_comp` 📖	—	`Topology.IsOpenEmbedding`	—	—	`of_comp_iff`
`of_comp_iff` 📖	—	`Topology.IsOpenEmbedding`	—	—	`Topology.IsEmbedding.continuous_iff` `toIsEmbedding` `Function.Injective.of_comp_iff` `Topology.IsEmbedding.injective` `isOpenMap_iff`
`of_continuous_injective_isOpenMap` 📖	mathematical	`Continuous` `IsOpenMap`	`Topology.IsOpenEmbedding`	—	`le_antisymm` `Filter.Tendsto.le_comap` `Continuous.tendsto` `Filter.comap_mono` `IsOpenMap.nhds_le` `Filter.comap_map`
`of_isEmbedding` 📖	mathematical	`Topology.IsEmbedding`	`Topology.IsOpenEmbedding`	—	`Topology.IsEmbedding.isOpenEmbedding_of_surjective`
`of_isEmbedding_isOpenMap` 📖	mathematical	`Topology.IsEmbedding` `IsOpenMap`	`Topology.IsOpenEmbedding`	—	`IsOpenMap.isOpen_range`
`of_isEmpty` 📖	mathematical	—	`Topology.IsOpenEmbedding`	—	`of_isEmbedding_isOpenMap` `Topology.IsEmbedding.of_subsingleton` `IsEmpty.instSubsingleton` `IsOpenMap.of_isEmpty`
`tendsto_nhds_iff` 📖	mathematical	`Topology.IsOpenEmbedding`	`Filter.Tendsto` `nhds`	—	`Topology.IsEmbedding.tendsto_nhds_iff` `isEmbedding`
`tendsto_nhds_iff'` 📖	mathematical	`Topology.IsOpenEmbedding`	`Filter.Tendsto` `nhds`	—	`Filter.Tendsto.eq_1` `Filter.map_map` `map_nhds_eq`

Topology.IsQuotientMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	—	`Topology.IsQuotientMap`	—	—	`surjective` `eq_coinduced` `coinduced_compose`
`continuous` 📖	mathematical	`Topology.IsQuotientMap`	`Continuous`	—	`continuous_iff` `continuous_id`
`continuous_iff` 📖	mathematical	`Topology.IsQuotientMap`	`Continuous`	—	`continuous_iff_coinduced_le` `eq_coinduced` `coinduced_compose`
`id` 📖	mathematical	—	`Topology.IsQuotientMap`	—	`coinduced_id`
`isClosed_preimage` 📖	mathematical	`Topology.IsQuotientMap`	`IsClosed` `Set.preimage`	—	`Topology.isQuotientMap_iff_isClosed`
`isOpen_preimage` 📖	mathematical	`Topology.IsQuotientMap`	`IsOpen` `Set.preimage`	—	`Topology.isQuotientMap_iff`
`of_comp` 📖	—	`Continuous` `Topology.IsQuotientMap`	—	—	`Function.Surjective.of_comp` `surjective` `le_antisymm` `eq_coinduced` `coinduced_compose` `le_imp_le_of_le_of_le` `coinduced_mono` `Continuous.coinduced_le` `le_refl`
`of_comp_isQuotientMap` 📖	—	`Topology.IsQuotientMap`	—	—	`of_comp_of_eq_coinduced` `eq_coinduced`
`of_comp_of_eq_coinduced` 📖	—	`Topology.IsQuotientMap` `TopologicalSpace.coinduced`	—	—	`Topology.isQuotientMap_iff` `Function.Surjective.of_comp` `surjective` `TopologicalSpace.ext_iff` `isOpen_coinduced`
`of_inverse` 📖	mathematical	`Continuous`	`Topology.IsQuotientMap`	—	`of_comp` `id` `Function.LeftInverse.comp_eq_id`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosedMap_iff_closure_image` 📖	mathematical	—	`IsClosedMap` `Set` `Set.instHasSubset` `closure` `Set.image`	—	`IsClosedMap.closure_image_subset` `isClosed_of_closure_subset` `IsClosed.closure_eq`
`isClosedMap_iff_clusterPt` 📖	mathematical	—	`IsClosedMap` `ClusterPt` `Filter.principal`	—	`Filter.map_principal`
`isClosedMap_iff_comap_nhdsSet_le` 📖	mathematical	—	`IsClosedMap` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.comap` `nhdsSet` `Set.preimage`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_rfl` `Set.instReflSubset`
`isClosedMap_iff_comap_nhds_le` 📖	mathematical	—	`IsClosedMap` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.comap` `nhds` `nhdsSet` `Set.preimage` `Set` `Set.instSingletonSet`	—	`isClosedMap_iff_comap_nhdsSet_le` `nhdsSet_singleton` `Set.biUnion_of_singleton` `Set.preimage_iUnion` `nhdsSet_iUnion` `Filter.comap_iSup` `iSup_congr_Prop` `iSup₂_mono`
`isClosedMap_iff_kernImage` 📖	mathematical	—	`IsClosedMap` `IsOpen` `Set.kernImage`	—	`IsClosedMap.eq_1` `Function.Surjective.forall` `compl_surjective` `Set.kernImage_eq_compl`
`isClosedMap_iff_kernImage_interior` 📖	mathematical	—	`IsClosedMap` `Set` `Set.instHasSubset` `Set.kernImage` `interior`	—	`isClosedMap_iff_closure_image` `Function.Surjective.forall` `compl_surjective` `closure_compl` `Set.kernImage_eq_compl` `interior_compl`
`isOpenMap_iff_closure_kernImage` 📖	mathematical	—	`IsOpenMap` `Set` `Set.instHasSubset` `closure` `Set.kernImage`	—	`isOpenMap_iff_image_interior` `Function.Surjective.forall` `compl_surjective` `interior_compl` `Set.kernImage_eq_compl` `closure_compl`
`isOpenMap_iff_clusterPt_comap` 📖	mathematical	—	`IsOpenMap` `ClusterPt` `Filter.comap`	—	`IsOpenMap.clusterPt_comap` `Mathlib.Tactic.Contrapose.contrapose₁` `mem_interior_iff_mem_nhds` `mem_interior_iff_not_clusterPt_compl` `ClusterPt.mono` `Filter.comap_principal`
`isOpenMap_iff_image_interior` 📖	mathematical	—	`IsOpenMap` `Set` `Set.instHasSubset` `Set.image` `interior`	—	`IsOpenMap.image_interior_subset` `subset_interior_iff_isOpen` `IsOpen.interior_eq`
`isOpenMap_iff_interior` 📖	mathematical	—	`IsOpenMap` `Set` `Set.instHasSubset` `Set.image` `interior`	—	`isOpenMap_iff_image_interior`
`isOpenMap_iff_kernImage` 📖	mathematical	—	`IsOpenMap` `IsClosed` `Set.kernImage`	—	`IsOpenMap.eq_1` `Function.Surjective.forall` `compl_surjective` `Set.kernImage_eq_compl`
`isOpenMap_iff_nhds_le` 📖	mathematical	—	`IsOpenMap` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds` `Filter.map`	—	`IsOpenMap.nhds_le` `IsOpenMap.of_nhds_le`

---

← Back to Index