ext — Mathlib

English

Let x,y be points in Euclidean Half-Space n. If their first coordinates are equal, then x equals y (assuming nonzero dimension).

Русский

Пусть x,y — точки в полупространстве Евклида n. Если их первые координаты равны, то x = y (при ненулевой размерности).

LaTeX

$$$\\forall n \\in \\mathbb{N}, [n>0] \\; x,y \\in \\mathrm{EuclideanHalfSpace}(n),\\; x_1 = y_1 \\Rightarrow x = y$$$

Lean4

@[ext]
theorem ext [NeZero n] (x y : EuclideanHalfSpace n) (h : x.1 = y.1) : x = y :=
  Subtype.eq h

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