coe_inj — Mathlib

English

For all x, y in R, (x : ℍ[R]) = (y : ℍ[R]) if and only if x = y; the coercion is injective.

Русский

Для всех x, y \\in R выполняется (x \\in \\mathbb{H}(R)) = (y \\in \\mathbb{H}(R)) тогда и только тогда, когда x = y; вложение инъективно.

LaTeX

$$$\\forall x \\forall y \\in R, (x : \\mathbb{H}(R)) = (y : \\mathbb{H}(R)) \\Leftrightarrow x = y$$$

Lean4

@[simp]
theorem coe_inj {x y : R} : (x : ℍ[R]) = y ↔ x = y :=
  coe_injective.eq_iff

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