Theorems · Theorem · general topology

prod_mem_nhds_iff

∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} {t : Set Y} {x : X}
  {y : Y}, s ×ˢ t ∈ nhds (x, y) ↔ s ∈ nhds x ∧ t ∈ nhds y

Defined in

Mathlib.Topology.Constructions.SumProd

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace