mem_uniformity_of_eq

Mathlib.Topology.UniformSpace.Defs

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

English

If s ∈ 𝓤 α and x = y, then (x, y) ∈ s.

Русский

Если s ∈ 𝓤 α и x = y, то (x, y) ∈ s.

LaTeX

$$$s\\in 𝓤 α \\land x=y \\Rightarrow (x,y)\\in s$$$

Lean4

theorem mem_uniformity_of_eq {x y : α} {s : Set (α × α)} (h : s ∈ 𝓤 α) (hx : x = y) : (x, y) ∈ s :=
  refl_le_uniformity h hx

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

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

Разделы

Аффилиация

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