nhdsSet_prod_le — Mathlib

English

The product of a neighborhood of s and a neighborhood of t is a neighborhood of s ×ˢ t.

Русский

Произведение окрестностей s и t является окрестностью s ×ˢ t.

LaTeX

$$$\nhdsSet (s \timesˢ t) \le \nhdsSet s \timesˢ \nhdsSet t$$$

Lean4

/-- 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. -/
theorem nhdsSet_prod_le (s : Set X) (t : Set Y) : 𝓝ˢ (s ×ˢ t) ≤ 𝓝ˢ s ×ˢ 𝓝ˢ t :=
  ((hasBasis_nhdsSet _).prod (hasBasis_nhdsSet _)).ge_iff.2 fun (_u, _v) ⟨⟨huo, hsu⟩, hvo, htv⟩ ↦
    (huo.prod hvo).mem_nhdsSet.2 <| prod_mono hsu htv

Похожие утверждения