Theorems · Theorem · general topology

UniformSpace.ball_mem_nhdsWithin

∀ {α : Type ua} [inst : UniformSpace α] {x : α} {S : Set α} ⦃V : SetRel α α⦄,
  x ∈ S → V ∈ uniformity α ⊓ Filter.principal (S ×ˢ S) → UniformSpace.ball x V ∈ nhdsWithin x S

Defined in

Mathlib.Topology.UniformSpace.Defs

Cited by

1 results in Mathlib

Foundations

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

Assumes

UniformSpace