mem_nhds_prod_iff' — Mathlib

English

The membership criterion for nhds of a product point: s ∈ 𝓝 (x,y) if and only if there exist open neighborhoods U of x and V of y with U × V ⊆ s.

Русский

Критерий принадлежности окрестности произведения: s ∈ 𝓝 (x,y) тогда, когда существуют открытые окрестности U около x и V около y, такие что U × V ⊆ s.

LaTeX

$$$ s ∈ 𝓝 (x, y) \\iff \\exists U,V, IsOpen U \\land x ∈ U \\land IsOpen V \\land y ∈ V \\land U ×ˢ V ⊆ s $$$

Lean4

theorem mem_nhds_prod_iff' {x : X} {y : Y} {s : Set (X × Y)} :
    s ∈ 𝓝 (x, y) ↔ ∃ u v, IsOpen u ∧ x ∈ u ∧ IsOpen v ∧ y ∈ v ∧ u ×ˢ v ⊆ s :=
  ((nhds_basis_opens x).prod_nhds (nhds_basis_opens y)).mem_iff.trans <| by
    simp only [Prod.exists, and_comm, and_assoc, and_left_comm]

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