ext

Mathlib.Analysis.Complex.UpperHalfPlane.Basic

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.ext

English

Extensionality principle: two points of the upper half-plane are equal if their complex coordinates are equal.

Русский

Принцип экстенсиональности: две точки ℍ равны, если их комплексные координаты равны.

LaTeX

$$$\forall a,b \in \mathbb{H}, a = b \text{ iff } a = b \text{ as complex numbers}$$$

Lean4

@[ext]
theorem ext {a b : ℍ} (h : (a : ℂ) = b) : a = b :=
  Subtype.eq h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru