Theorems · Definition · general topology

Homeomorph.quotientKerEquivRange

{X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {f : X → Y} → Topology.IsStrictMap f → Quotient (Setoid.ker f) ≃ₜ ↑(Set.range f)

The homeomorphism Quotient (Setoid.ker f) ≃ₜ Set.range f given by a strict map f. This is the homeomorphism obtained from the first isomorphism theorem.

Defined in

Mathlib.Topology.Maps.Strict.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace