Mathlib Map

Theorems · Theorem · general topology

IsOpenMap.id

∀ {X : Type u_1} [inst : TopologicalSpace X], IsOpenMap id
Defined in
Mathlib.Topology.Maps.Basic
Cited by
12 results in Mathlib
Foundations
Depth 9 from the axioms · uses propext, Quot.sound
Assumes
TopologicalSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

IsOpenQuotientMap.id · cited by 4IsOpenQuotientMap.idContinuousOpenMap.id · cited by 4ContinuousOpenMap.idIsHomeomorph.id · cited by 2IsHomeomorph.idTopology.IsOpenEmbedding.id · cited by 1IsOpenEmbedding.idTopologicalSpace.CompactOpens.map_id · cited by 0CompactOpens.map_idTopologicalSpace.PositiveCompacts.map_id · cited by 0PositiveCompacts.map_idIsOpen.isOpenMap_inclusion · cited by 0IsOpen.isOpenMap_inclusionisOpenMap_toAdd · cited by 0isOpenMap_toAddisOpenMap_toDual · cited by 0isOpenMap_toDualisOpenMap_toMul · cited by 0isOpenMap_toMulisOpenMap_ofAdd · cited by 0isOpenMap_ofAddisOpenMap_ofDual · cited by 0isOpenMap_ofDualisOpenMap_ofMul · cited by 0isOpenMap_ofMulSet · cited by 53352SetTopologicalSpace · cited by 24529TopologicalSpaceIsOpen · cited by 2400IsOpenIsOpenMap · cited by 253IsOpenMapSet.image_id · cited by 60Set.image_idIsOpenMap.idCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by13

Results whose statement or proof uses this declaration.