ext — Mathlib

English

Elements of Unitization R A are determined by their fst and snd components; equality is given by equality of fst and snd coordinates.

Русский

Элементы Unitization R A задаются двумя координатами, fst и snd; равенство определяется по равенству этих координат.

LaTeX

$$$\\\\forall x,y : Unitization R A, x = y \\\\Leftrightarrow x.fst = y.fst \\\\text{ и } x.snd = y.snd.$$$

Lean4

@[ext]
theorem ext {x y : Unitization R A} (h1 : x.fst = y.fst) (h2 : x.snd = y.snd) : x = y :=
  Prod.ext h1 h2

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