prod_mem_nhds

Mathlib.Topology.Constructions.SumProd

URI: https://scilib.ai/kg/mathlib#prod_mem_nhds

English

If s ∈ 𝓝 x and t ∈ 𝓝 y, then s × t ∈ 𝓝 (x,y).

Русский

Если s ∈ 𝓝 x и t ∈ 𝓝 y, то s × t ∈ 𝓝 (x,y).

LaTeX

$$$ s \\in 𝓝 x \\quad \\&\\quad t \\in 𝓝 y \\Rightarrow s \\timesˢ t \\in 𝓝 (x, y) $$$

Lean4

theorem prod_mem_nhds {s : Set X} {t : Set Y} {x : X} {y : Y} (hx : s ∈ 𝓝 x) (hy : t ∈ 𝓝 y) : s ×ˢ t ∈ 𝓝 (x, y) :=
  prod_mem_nhds_iff.2 ⟨hx, hy⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru