coe_eq_zero_iff — Mathlib

English

If α is a uniform space with a zero and is T0, then the canonical embedding α → Completion α is injective; equivalently, for every x ∈ α, (x in Completion α) = 0 iff x = 0.

Русский

Пусть α — равномерное пространство с нулём и удовлетворяет условию T0. Тогда каноническое вложение α в Completion α инъективно; то есть для каждого x ∈ α выполняется (x → Completion α) = 0 тогда и только тогда, когда x = 0.

LaTeX

$$$\\forall x\\in\\alpha,\\ (x : \\mathrm{Completion}(\\alpha)) = 0 \\iff x = 0$$$

Lean4

@[simp]
theorem coe_eq_zero_iff [Zero α] [T0Space α] {x : α} : (x : Completion α) = 0 ↔ x = 0 :=
  Completion.coe_inj

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