Theorems · Theorem · complex analysis
ValueDistribution.proximity_mul_zero_le
∀ {f₁ f₂ : ℂ → ℂ},
Meromorphic f₁ →
Meromorphic f₂ →
ValueDistribution.proximity (f₁ * f₂) 0 ≤ ValueDistribution.proximity f₁ 0 + ValueDistribution.proximity f₂ 0The proximity function f * g at 0 is less than or equal to the sum of the proximity functions of
f and g, respectively.
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 273 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Top.topproof · cited by 9,680
- Complexstatement and proof · cited by 5,565
- WithTopstatement · cited by 3,754
- Meromorphicstatement and proof · cited by 108
- mul_invproof · cited by 50
- ValueDistribution.proximitystatement and proof · cited by 28
- Meromorphic.invproof · cited by 3
- ValueDistribution.proximity_invproof · cited by 2
- ValueDistribution.proximity_mul_top_leproof · cited by 2
Cited by1
Results whose statement or proof uses this declaration.
- ValueDistribution.characteristic_mul_zero_leproof · cited by 1