ext — Mathlib

English

Two nonnegative rationals are equal if their rational parts are equal; extensionality for the subtype.

Русский

Две неотрицательные рациональные числа равны тогда и только тогда, когда их рациональные части равны; экстенсивность подпредела.

LaTeX

$$$(p : \mathbb{Q}) = (q : \mathbb{Q}) \Rightarrow p = q$$$

Lean4

@[ext]
theorem ext : (p : ℚ) = (q : ℚ) → p = q :=
  Subtype.ext

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