refl_mem_uniformity

Mathlib.Topology.UniformSpace.Defs

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

English

If s is in the uniformity, then (x, x) ∈ s for any x.

Русский

Если s в равномерности, то для любого x верно (x, x) ∈ s.

LaTeX

$$$\\forall x:\\; α,\\; \\forall s\\in 𝓤 α,\\; (x,x)\\in s$$$

Lean4

theorem refl_mem_uniformity {x : α} {s : Set (α × α)} (h : s ∈ 𝓤 α) : (x, x) ∈ s :=
  refl_le_uniformity h rfl

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

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

Разделы

Аффилиация

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