Theorems · Theorem · general topology

OpenPartialHomeomorph.continuous_iff_continuous_comp_left

∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Z → X},
  f ⁻¹' e.source = Set.univ → (Continuous f ↔ Continuous (↑e ∘ f))

A function is continuous if and only if its composition with an open partial homeomorphism on the left is continuous and its image is contained in the source.

Defined in

Mathlib.Topology.OpenPartialHomeomorph.Continuity

Cited by

1 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpace