dist_comm

Mathlib.Analysis.Complex.UpperHalfPlane.Metric

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

English

Distance in the upper half-plane is symmetric: dist(z,w) = dist(w,z).

Русский

Расстояние в верхней полуплоскости симметрично: dist(z,w) = dist(w,z).

LaTeX

$$$dist(z,w) = dist(w,z)$$$

Lean4

protected theorem dist_comm (z w : ℍ) : dist z w = dist w z := by simp only [dist_eq, dist_comm (z : ℂ), mul_comm]

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

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

Разделы

Аффилиация

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