ext_val — Mathlib

English

If two elements of a subtype have equal underlying values, they are equal as subtype elements.

Русский

Если два элемента подтипа имеют равные основания, они равны как элементы подтипа.

LaTeX

$$$\\forall a_1,a_2 : \\{x\\;|\\;p x\\},\\; a_1.1 = a_2.1 \\Rightarrow a_1 = a_2.$$$

Lean4

@[deprecated Subtype.ext (since := "2025-09-10")]
theorem ext_val {a1 a2 : { x // p x }} : a1.1 = a2.1 → a1 = a2 :=
  Subtype.ext

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