Theorems · Theorem · geometry

UpperHalfPlane.sinh_half_dist_add_dist

∀ (a b c : UpperHalfPlane),
  Real.sinh ((dist a b + dist b c) / 2) =
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) /
      (2 * √(a.im * c.im) * dist (↑b) ((starRingEnd ℂ) ↑b))

Defined in: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Cited by: 1 results in Mathlib
Foundations: Depth 177 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites28

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Realstatement and proof · cited by 25,697
RingHomstatement · cited by 10,189
Complexstatement and proof · cited by 5,565
mul_commproof · cited by 2,262
LT.lt.leproof · cited by 2,189
absproof · cited by 1,814
Dist.diststatement and proof · cited by 1,539
starRingEndstatement and proof · cited by 671
UpperHalfPlanestatement and proof · cited by 626
Real.sqrtstatement and proof · cited by 545
UpperHalfPlane.coestatement and proof · cited by 288

Cited by1

Results whose statement or proof uses this declaration.

UpperHalfPlane.dist_triangleproof · cited by 0