OpenQuotient

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

Statistics

Metric	Count
Definitions	0
Theorems baireSpace, comp, continuousAt_comp_iff, continuous_comp_iff, dense_preimage_iff, id, iff_isOpenMap_isQuotientMap, isQuotientMap, map_nhds_eq, of_isOpenMap_isQuotientMap, isOpenQuotientMap_of_surjective, isQuotientMap_of_surjective, coinduced_eq_induced_of_isOpenQuotientMap_of_isInducing, isEmbedding_of_isOpenQuotientMap_of_isInducing, isQuotientMap_of_isOpenQuotientMap_of_isInducing	15
Total	15

IsOpenQuotientMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baireSpace 📖	mathematical	IsOpenQuotientMap	BaireSpace	—	dense_iInter_of_isOpen_nat Continuous.isOpen_preimage continuous dense_preimage_iff
comp 📖	—	IsOpenQuotientMap	—	—	surjective Continuous.comp continuous IsOpenMap.comp isOpenMap
continuousAt_comp_iff 📖	mathematical	IsOpenQuotientMap	ContinuousAt	—	map_nhds_eq
continuous_comp_iff 📖	mathematical	IsOpenQuotientMap	Continuous	—	Topology.IsQuotientMap.continuous_iff isQuotientMap
dense_preimage_iff 📖	mathematical	IsOpenQuotientMap	Dense Set.preimage	—	DenseRange.dense_of_mapsTo Function.Surjective.denseRange surjective continuous Set.mapsTo_preimage Dense.preimage isOpenMap
id 📖	mathematical	—	IsOpenQuotientMap	—	continuous_id IsOpenMap.id
iff_isOpenMap_isQuotientMap 📖	mathematical	—	IsOpenQuotientMap IsOpenMap Topology.IsQuotientMap	—	isOpenMap isQuotientMap Topology.IsQuotientMap.surjective Topology.IsQuotientMap.continuous
isQuotientMap 📖	mathematical	IsOpenQuotientMap	Topology.IsQuotientMap	—	IsOpenMap.isQuotientMap isOpenMap continuous surjective
map_nhds_eq 📖	mathematical	IsOpenQuotientMap	Filter.map nhds	—	le_antisymm Continuous.continuousAt continuous IsOpenMap.nhds_le isOpenMap
of_isOpenMap_isQuotientMap 📖	mathematical	IsOpenMap Topology.IsQuotientMap	IsOpenQuotientMap	—	iff_isOpenMap_isQuotientMap

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isOpenQuotientMap_of_surjective 📖	mathematical	Topology.IsInducing	IsOpenQuotientMap	—	continuous isOpen_iff Set.image_preimage_eq
isQuotientMap_of_surjective 📖	mathematical	Topology.IsInducing	Topology.IsQuotientMap	—	IsOpenQuotientMap.isQuotientMap isOpenQuotientMap_of_surjective

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coinduced_eq_induced_of_isOpenQuotientMap_of_isInducing 📖	mathematical	Topology.IsInducing IsOpenQuotientMap Set Set.instHasSubset Set.preimage Set.image Set.range	TopologicalSpace.coinduced TopologicalSpace.induced	—	TopologicalSpace.ext Topology.IsInducing.isOpen_iff Function.Surjective.exists Set.image_surjective IsOpenQuotientMap.surjective Topology.IsQuotientMap.isOpen_preimage IsOpenQuotientMap.isQuotientMap Continuous.isOpen_preimage IsOpenQuotientMap.continuous IsOpenQuotientMap.isOpenMap Set.ext Eq.le Eq.ge
isEmbedding_of_isOpenQuotientMap_of_isInducing 📖	mathematical	Topology.IsInducing Topology.IsQuotientMap IsOpenQuotientMap Set Set.instHasSubset Set.preimage Set.image Set.range	Topology.IsEmbedding	—	Topology.IsQuotientMap.eq_coinduced coinduced_eq_induced_of_isOpenQuotientMap_of_isInducing Topology.IsQuotientMap.surjective
isQuotientMap_of_isOpenQuotientMap_of_isInducing 📖	mathematical	Topology.IsInducing IsOpenQuotientMap Topology.IsEmbedding Set Set.instHasSubset Set.preimage Set.image Set.range	Topology.IsQuotientMap	—	Topology.IsInducing.eq_induced Topology.IsEmbedding.toIsInducing coinduced_eq_induced_of_isOpenQuotientMap_of_isInducing Topology.IsEmbedding.injective

---

← Back to Index