ext'

Mathlib.Analysis.Complex.UpperHalfPlane.Basic

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

← MathLib Explorer

English

Extensionality lemma in terms of UpperHalfPlane.re and UpperHalfPlane.im.

Русский

Лемма экстенсиональности в терминах re и im для UpperHalfPlane.

LaTeX

$$$\text{ext}'\{a,b:\mathbb{H}\} (a.re = b.re) (a.im = b.im) : a = b$$$

Lean4

/-- Extensionality lemma in terms of `UpperHalfPlane.re` and `UpperHalfPlane.im`. -/
theorem ext' {a b : ℍ} (hre : a.re = b.re) (him : a.im = b.im) : a = b :=
  ext <| Complex.ext hre him

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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