nhds_le_uniformity — Mathlib

English

If x and y are inseparable in α, then the neighborhood filter 𝓝(x,y) of the pair (x,y) in α×α is contained in the uniformity 𝓤α.

Русский

Если x и y неразделимы в α, то фильтр окрестностей 𝓝(x,y) в α×α содержится в 𝓤α.

LaTeX

$$$\text{Inseparable}(x,y) \rightarrow 𝓝(x,y) \le 𝓤(α)$$$

Lean4

protected theorem nhds_le_uniformity {x y : α} (h : Inseparable x y) : 𝓝 (x, y) ≤ 𝓤 α :=
  by
  rw [h.prod rfl]
  apply nhds_le_uniformity

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