kebekus
/
nevanlinna
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update holomorphic_primitive2.lean

This commit is contained in:
Stefan Kebekus 2024-08-07 09:21:25 +02:00
parent a2d3793df2
commit c3289f89c7
1 changed files with 10 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
Nevanlinna/holomorphic_primitive2.lean
View File

@ -303,10 +303,18 @@ theorem primitive_additivity
let εx := rx - dist z₀.re z₁.re let εx := rx - dist z₀.re z₁.re
have hεx : εx > 0 := by have hεx : εx > 0 := by
sorry let A := hz₁.1
simp at A
dsimp [εx]
rw [dist_comm]
simpa
let εy := ry - dist z₀.im z₁.im let εy := ry - dist z₀.im z₁.im
have hεy : εy > 0 := by have hεy : εy > 0 := by
sorry let A := hz₁.2
simp at A
dsimp [εy]
rw [dist_comm]
simpa
use εx use εx
use hεx use hεx