Theorems · Theorem · general topology

preStoneCechCompat

∀ {α : Type u} [inst : TopologicalSpace α] {β : Type v} [inst_1 : TopologicalSpace β] [T2Space β] [CompactSpace β]
  {g : α → β},
  Continuous g →
    ∀ {F G : Ultrafilter α} {x : α}, ↑F ≤ nhds x → ↑G ≤ nhds x → Ultrafilter.extend g F = Ultrafilter.extend g G

Defined in

Mathlib.Topology.Compactification.StoneCech

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceT2SpaceCompactSpace