mem_uniformity_ofCore_iff — Mathlib

English

A set s belongs to the uniformity of a core if and only if it belongs to the core's uniformity.

Русский

Множество s принадлежит равномерности ядра тогда и только тогда, когда оно принадлежит равномерности ядра.

LaTeX

$$$\\forall {u : UniformSpace.Core\\,\\alpha}\\; {s : Set(\\alpha\\times\\alpha)}:\\; s \\in 𝓤[.ofCore u] \\iff s \\in u.uniformity$$$

Lean4

theorem mem_uniformity_ofCore_iff {u : UniformSpace.Core α} {s : Set (α × α)} : s ∈ 𝓤[.ofCore u] ↔ s ∈ u.uniformity :=
  Iff.rfl

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