Theorems · Theorem · general topology

exists_nhds_square

∀ {X : Type u} [inst : TopologicalSpace X] {s : Set (X × X)} {x : X},
  s ∈ nhds (x, x) → ∃ U, IsOpen U ∧ x ∈ U ∧ U ×ˢ U ⊆ s

Given a neighborhood s of (x, x), then (x, x) has a square open neighborhood that is a subset of s.

Defined in

Mathlib.Topology.Constructions.SumProd

Cited by

3 results in Mathlib

Foundations

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

Assumes

TopologicalSpace