working…

2024-08-02 07:16:38 +02:00 · 2024-08-02 07:16:38 +02:00 · 2e5d008857
parent 78de1bd3b0
commit 2e5d008857
1 changed files with 5 additions and 0 deletions
--- a/Nevanlinna/holomorphic_primitive2.lean
+++ b/Nevanlinna/holomorphic_primitive2.lean
@ -363,6 +363,11 @@ theorem primitive_additivity
    apply DifferentiableOn.mono hf
    intro x hx
    simp
+    
+    let A₀ : dist x.re z₀.re ≤ dist x.re z₁.re + dist z₁.re z₀.re := by apply dist_triangle
+    
+
+

    sorry