coe_ne_coe — Mathlib

English

Equality or inequality of underlying elements corresponds to the same relation on subtypes: (a.α ≠ b.α) ↔ (a ≠ b).

Русский

Неравенство/равенство базовых элементов эквивалентно такому же отношению между подтипами: (a.α ≠ b.α) ↔ (a ≠ b).

LaTeX

$$$\forall a,b : Subtype\, p,\ (a : \alpha) \neq (b : \alpha) \iff a \neq b.$$$

Lean4

theorem coe_ne_coe {a b : Subtype p} : (a : α) ≠ b ↔ a ≠ b :=
  coe_injective.ne_iff

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