English
If s and t are compact and n is an open set with s × t ⊆ n, then there exist open u ⊇ s and v ⊇ t with u × v ⊆ n.
Русский
Если s и t компактны, а n — открытое множество, содержащее s × t, то существуют открытые окрестности u ⊇ s и v ⊇ t такие, что u × v ⊆ n.
LaTeX
$$$\exists u \; \exists v \\; (\text{IsOpen}(u) ∧ \text{IsOpen}(v) ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n)$$$
Lean4
/-- 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`. -/
theorem generalized_tube_lemma (hs : IsCompact s) {t : Set Y} (ht : IsCompact t) {n : Set (X × Y)} (hn : IsOpen n)
(hp : s ×ˢ t ⊆ n) : ∃ (u : Set X) (v : Set Y), IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n :=
by
rw [← hn.mem_nhdsSet, hs.nhdsSet_prod_eq ht, ((hasBasis_nhdsSet _).prod (hasBasis_nhdsSet _)).mem_iff] at hp
rcases hp with ⟨⟨u, v⟩, ⟨⟨huo, hsu⟩, hvo, htv⟩, hn⟩
exact
⟨u, v, huo, hvo, hsu, htv, hn⟩
-- see Note [lower instance priority]
