SeparatedMap

📁 Source: Mathlib/Topology/SeparatedMap.lean

Statistics

Metric	Count
Definitions IsLocallyInjective, IsSeparatedMap	2
Theorems mapPullback, IsLocallyInjective, isSeparatedMap, comp_left, comp_right, isOpen_eqLocus, IsLocallyInjective_iff_isOpenEmbedding, comp_left, comp_right, constOn_of_comp, const_of_comp, eqOn_of_comp_eqOn, eq_of_comp_eq, isClosed_eqLocus, pullback, isSeparatedMap, toPullbackDiag, discreteTopology_iff_locallyInjective, isLocallyInjective_iff_isOpenMap, isLocallyInjective_iff_isOpen_diagonal, isLocallyInjective_iff_nhds, isSeparatedMap_iff_disjoint_nhds, isSeparatedMap_iff_isClosedEmbedding, isSeparatedMap_iff_isClosedMap, isSeparatedMap_iff_isClosed_diagonal, isSeparatedMap_iff_nhds, t2space_iff_isSeparatedMap	27
Total	29

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapPullback 📖	mathematical	Continuous	Function.Pullback instTopologicalSpaceSubtype instTopologicalSpaceProd Function.mapPullback	—	continuous_induced_rng prodMk comp continuous_fst continuous_subtype_val continuous_snd

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IsLocallyInjective 📖	mathematical	—	IsLocallyInjective	—	isOpen_univ
isSeparatedMap 📖	mathematical	—	IsSeparatedMap	—	—

IsLocallyInjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_left 📖	—	IsLocallyInjective	—	—	Function.Injective.comp_injOn
comp_right 📖	—	IsLocallyInjective Continuous	—	—	isLocallyInjective_iff_isOpen_diagonal Function.Injective.preimage_pullbackDiagonal IsOpen.preimage Continuous.mapPullback
isOpen_eqLocus 📖	mathematical	Continuous IsLocallyInjective	IsOpen setOf	—	IsOpen.preimage Continuous.prodMk isLocallyInjective_iff_isOpen_diagonal

IsSeparatedMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_left 📖	—	IsSeparatedMap	—	—	—
comp_right 📖	—	IsSeparatedMap Continuous	—	—	isSeparatedMap_iff_isClosed_diagonal Function.Injective.preimage_pullbackDiagonal IsClosed.preimage Continuous.mapPullback
constOn_of_comp 📖	—	IsSeparatedMap IsLocallyInjective IsPreconnected ContinuousOn Set Set.instMembership	—	—	eqOn_of_comp_eqOn Continuous.continuousOn continuous_const
const_of_comp 📖	—	IsSeparatedMap IsLocallyInjective Continuous	—	—	eq_of_comp_eq continuous_const
eqOn_of_comp_eqOn 📖	—	IsSeparatedMap IsLocallyInjective IsPreconnected ContinuousOn Set.EqOn Set Set.instMembership	—	—	Set.restrict_eq_restrict_iff eq_of_comp_eq isPreconnected_iff_preconnectedSpace continuousOn_iff_continuous_restrict
eq_of_comp_eq 📖	—	IsSeparatedMap IsLocallyInjective Continuous	—	—	Set.mem_univ IsClopen.eq_univ isClosed_eqLocus IsLocallyInjective.isOpen_eqLocus
isClosed_eqLocus 📖	mathematical	Continuous IsSeparatedMap	IsClosed setOf	—	IsClosed.preimage Continuous.prodMk isSeparatedMap_iff_isClosed_diagonal
pullback 📖	mathematical	IsSeparatedMap	Function.Pullback instTopologicalSpaceSubtype instTopologicalSpaceProd Function.Pullback.snd	—	isSeparatedMap_iff_isClosed_diagonal preimage_map_fst_pullbackDiagonal IsClosed.preimage Function.pullback_comm_sq Continuous.mapPullback Continuous.comp continuous_fst continuous_subtype_val

T2Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSeparatedMap 📖	mathematical	—	IsSeparatedMap	—	t2_separation

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toPullbackDiag 📖	mathematical	—	Topology.IsEmbedding Function.Pullback instTopologicalSpaceSubtype instTopologicalSpaceProd toPullbackDiag	—	mk' injective_toPullbackDiag nhds_induced nhds_prod_eq Filter.comap_prod Filter.comap_inf Filter.comap_comap Filter.comap_id' inf_of_le_left

(root)

Definitions

Name	Category	Theorems
IsLocallyInjective 📖	MathDef	7 math math: discreteTopology_iff_locallyInjective, isLocallyInjective_iff_isOpen_diagonal, isLocallyInjective_iff_isOpenMap, Function.Injective.IsLocallyInjective, IsLocallyInjective_iff_isOpenEmbedding, IsLocalHomeomorph.isLocallyInjective, isLocallyInjective_iff_nhds
IsSeparatedMap 📖	MathDef	9 math math: isSeparatedMap_iff_disjoint_nhds, T2Space.isSeparatedMap, isSeparatedMap_iff_isClosedEmbedding, isSeparatedMap_iff_isClosedMap, t2space_iff_isSeparatedMap, Function.Injective.isSeparatedMap, isSeparatedMap_iff_nhds, IsCoveringMap.isSeparatedMap, isSeparatedMap_iff_isClosed_diagonal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IsLocallyInjective_iff_isOpenEmbedding 📖	mathematical	—	IsLocallyInjective Topology.IsOpenEmbedding Function.Pullback instTopologicalSpaceSubtype instTopologicalSpaceProd toPullbackDiag	—	isLocallyInjective_iff_isOpen_diagonal range_toPullbackDiag Topology.IsEmbedding.toPullbackDiag Topology.IsOpenEmbedding.isOpen_range
discreteTopology_iff_locallyInjective 📖	mathematical	—	DiscreteTopology IsLocallyInjective	—	discreteTopology_iff_singleton_mem_nhds isLocallyInjective_iff_nhds Set.injOn_singleton Set.ext mem_of_mem_nhds
isLocallyInjective_iff_isOpenMap 📖	mathematical	—	IsLocallyInjective IsOpenMap Function.Pullback instTopologicalSpaceSubtype instTopologicalSpaceProd toPullbackDiag	—	IsLocallyInjective_iff_isOpenEmbedding Topology.IsOpenEmbedding.isOpenMap Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap Topology.IsEmbedding.continuous Topology.IsEmbedding.toPullbackDiag injective_toPullbackDiag
isLocallyInjective_iff_isOpen_diagonal 📖	mathematical	—	IsLocallyInjective IsOpen Function.Pullback instTopologicalSpaceSubtype instTopologicalSpaceProd Function.pullbackDiagonal	—	nhds_induced nhds_prod_eq Filter.prod_mem_prod Filter.mem_prod_iff Filter.inter_mem
isLocallyInjective_iff_nhds 📖	mathematical	—	IsLocallyInjective Set Filter Filter.instMembership nhds Set.InjOn	—	IsOpen.mem_nhds isOpen_interior mem_interior_iff_mem_nhds Set.InjOn.mono interior_subset
isSeparatedMap_iff_disjoint_nhds 📖	mathematical	—	IsSeparatedMap Disjoint Filter Filter.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder Filter.instCompleteLatticeFilter nhds	—	Filter.HasBasis.disjoint_iff nhds_basis_opens
isSeparatedMap_iff_isClosedEmbedding 📖	mathematical	—	IsSeparatedMap Topology.IsClosedEmbedding Function.Pullback instTopologicalSpaceSubtype instTopologicalSpaceProd toPullbackDiag	—	isSeparatedMap_iff_isClosed_diagonal range_toPullbackDiag Topology.IsEmbedding.toPullbackDiag Topology.IsClosedEmbedding.isClosed_range
isSeparatedMap_iff_isClosedMap 📖	mathematical	—	IsSeparatedMap IsClosedMap Function.Pullback instTopologicalSpaceSubtype instTopologicalSpaceProd toPullbackDiag	—	isSeparatedMap_iff_isClosedEmbedding Topology.IsClosedEmbedding.isClosedMap Topology.IsClosedEmbedding.of_continuous_injective_isClosedMap Topology.IsEmbedding.continuous Topology.IsEmbedding.toPullbackDiag injective_toPullbackDiag
isSeparatedMap_iff_isClosed_diagonal 📖	mathematical	—	IsSeparatedMap IsClosed Function.Pullback instTopologicalSpaceSubtype instTopologicalSpaceProd Function.pullbackDiagonal	—	nhds_induced nhds_prod_eq subset_rfl Set.instReflSubset Filter.mem_prod_iff Set.disjoint_left
isSeparatedMap_iff_nhds 📖	mathematical	—	IsSeparatedMap Set Filter Filter.instMembership nhds Disjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	—
t2space_iff_isSeparatedMap 📖	mathematical	—	T2Space IsSeparatedMap	—	—

---

← Back to Index