Theorems · Theorem · general topology

generalized_tube_lemma

∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X},
  IsCompact s →
    ∀ {t : Set Y},
      IsCompact t → ∀ {n : Set (X × Y)}, IsOpen n → s ×ˢ t ⊆ n → ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n

If s and t are compact sets and n is an open neighborhood of s × t, then there exist open neighborhoods u ⊇ s and v ⊇ t such that u × v ⊆ n. See also IsCompact.nhdsSet_prod_eq.

Defined in

Mathlib.Topology.Compactness.Compact

Cited by

6 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace