ext — Mathlib

English

Two points on the circle are equal if and only if their underlying complex coordinates are equal; the circle is determined by its complex coordinate.

Русский

Две точки на окружности равны тогда и только тогда, когда равны их комплексные координаты; окружность определяется её комплексной координатой.

LaTeX

$$$$ \\forall x,y \\in \\mathbb{S}^1, \\ (x \\;\\mathrm{val} = y \\;\\mathrm{val}) \\iff x = y. $$$$

Lean4

@[ext]
theorem ext : (x : ℂ) = y → x = y :=
  Subtype.ext

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