Theorems · Theorem · general topology

Disjoint.exists_uniform_thickening

∀ {α : Type ua} [inst : UniformSpace α] {A B : Set α},
  IsCompact A →
    IsClosed B →
      Disjoint A B → ∃ V ∈ uniformity α, Disjoint (⋃ x ∈ A, UniformSpace.ball x V) (⋃ x ∈ B, UniformSpace.ball x V)

Defined in

Mathlib.Topology.UniformSpace.Compact

Cited by

1 results in Mathlib

Foundations

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

Assumes

UniformSpace