exists_nhds_square — Mathlib

English

Given a neighborhood s of (x,x) in X × X, there exists an open square neighborhood U × U with x ∈ U and U × U ⊆ s.

Русский

Для окрестности s точки (x,x) в X × X существует открытая окрестность-«квадрат» U × U с x ∈ U и U × U ⊆ s.

LaTeX

$$$$\exists U\subseteq X,\IsOpen(U) \land x\in U \land U\times U \subseteq s.$$$$

Lean4

/-- Given a neighborhood `s` of `(x, x)`, then `(x, x)` has a square open neighborhood
  that is a subset of `s`. -/
theorem exists_nhds_square {s : Set (X × X)} {x : X} (hx : s ∈ 𝓝 (x, x)) : ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ U ×ˢ U ⊆ s :=
  by simpa [nhds_prod_eq, (nhds_basis_opens x).prod_self.mem_iff, and_assoc, and_left_comm] using hx

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