Theorems · Theorem · general topology

IsLocallyInjective.isOpen_eqLocus

∀ {X : Type u_1} {Y : Type u_2} {A : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace A] {f : X → Y}
  {g₁ g₂ : A → X}, Continuous g₁ → Continuous g₂ → IsLocallyInjective f → f ∘ g₁ = f ∘ g₂ → IsOpen {a | g₁ a = g₂ a}

Defined in

Mathlib.Topology.SeparatedMap

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace