Theorems · Theorem · general topology

isClosed_range_of_spaced_out

∀ {α : Type u} [inst : UniformSpace α] {ι : Type u_1} [T0Space α] {V₀ : Set (α × α)},
  V₀ ∈ uniformity α → ∀ {f : ι → α}, (Pairwise fun x y => (f x, f y) ∉ V₀) → IsClosed (Set.range f)

Defined in

Mathlib.Topology.UniformSpace.Separation

Cited by

1 results in Mathlib

Foundations

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

Assumes

UniformSpaceT0Space