Theorems · Theorem · general topology
Continuous.isOpen_preimage
∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
Continuous f → ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)The preimage of an open set under a continuous function is an open set. Use IsOpen.preimage
instead.
- Defined in
- Mathlib.Topology.Defs.Basic
- Cited by
- 51 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Set.preimagestatement · cited by 4,946
- Continuousstatement and proof · cited by 2,592
- IsOpenstatement · cited by 2,400
Cited by51
Results whose statement or proof uses this declaration.
- IsOpen.preimageproof · cited by 147
- continuous_defproof · cited by 21
- Metric.isOpen_thickeningproof · cited by 11
- Complex.differentiableAt_Gammaproof · cited by 8
- TopologicalSpace.Compacts.isOpen_subsets_of_isOpenproof · cited by 7
- hasFDerivAt_jacobiTheta₂proof · cited by 4
- IsLocallyConstant.iff_continuousproof · cited by 4
- TopologicalSpace.Compacts.isOpen_inter_nonempty_of_isOpenproof · cited by 4
- Topology.WithGeneratedByTopology.continuous_equivproof · cited by 4
- IsCoveringMap.isSeparatedMapproof · cited by 4
- AddMonoidHom.isOpenQuotientMap_of_isQuotientMapproof · cited by 3
- PeriodPair.summable_weierstrassPExceptSummandproof · cited by 3