Theorems · Theorem · general topology

nhdsSet_prod_le

∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (s : Set X) (t : Set Y),
  nhdsSet (s ×ˢ t) ≤ nhdsSet s ×ˢ nhdsSet t

The product of a neighborhood of s and a neighborhood of t is a neighborhood of s ×ˢ t, formulated in terms of a filter inequality.

Defined in

Mathlib.Topology.Constructions

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace