Theorems · Theorem · general topology

TotallyDisconnectedSpace.continuousMapEquivOfConnectedSpace_symm_apply_apply

∀ (X : Type u_3) (Y : Type u_4) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TotallyDisconnectedSpace Y] [inst_3 : ConnectedSpace X] (y : Y) (x : X),
  ((TotallyDisconnectedSpace.continuousMapEquivOfConnectedSpace X Y).symm y) x = y

Defined in

Mathlib.Topology.Connected.TotallyDisconnected

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTotallyDisconnectedSpaceConnectedSpace