Theorems · Theorem · general topology
IsOpenMap.isOpen_range
∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
IsOpenMap f → IsOpen (Set.range f)- Defined in
- Mathlib.Topology.Maps.Basic
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Set.rangestatement · cited by 4,705
- Set.univproof · cited by 3,945
- IsOpenstatement and proof · cited by 2,400
- Set.image_univproof · cited by 322
- IsOpenMapstatement and proof · cited by 253
- isOpen_univproof · cited by 112
Cited by11
Results whose statement or proof uses this declaration.
- Topology.IsOpenEmbedding.compproof · cited by 12
- Topology.IsOpenEmbedding.of_isEmbedding_isOpenMapproof · cited by 4
- isOpen_range_sigmaMkproof · cited by 2
- Topology.IsOpenEmbedding.idproof · cited by 1
- preimage_mem_irreducibleComponents_of_isPreirreducible_fiberproof · cited by 1
- IsOpenMap.separableSpace_of_isInducingproof · cited by 0
- AlgebraicGeometry.IsOpenImmersion.of_flat_of_monoproof · cited by 0
- IsOpenMap.denseRange_of_isPreirreducibleSpaceproof · cited by 0
- closure_image_preimage_of_isPreirreducibleproof · cited by 0
- IsLocalDiffeomorph.isOpen_rangeproof · cited by 0
- IsOpenMap.range_mem_nhdsproof · cited by 0