Theorems · Theorem · general topology

eq_if_stoneCechUnit_eq

∀ {α : Type u} [inst : TopologicalSpace α] {β : Type v} [inst_1 : TopologicalSpace β] [T2Space β] [CompactSpace β]
  {a b : α} {f : α → β}, Continuous f → stoneCechUnit a = stoneCechUnit b → f a = f b

Defined in

Mathlib.Topology.Compactification.StoneCech

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceT2SpaceCompactSpace