Theorems · Theorem · complex analysis
ValueDistribution.proximity_mul_top_le
∀ {f₁ f₂ : ℂ → ℂ},
Meromorphic f₁ →
Meromorphic f₂ →
ValueDistribution.proximity (f₁ * f₂) ⊤ ≤ ValueDistribution.proximity f₁ ⊤ + ValueDistribution.proximity f₂ ⊤The proximity function f * g at ⊤ is less than or equal to the sum of the proximity functions of
f and g, respectively.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 272 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
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.topstatement and proof · cited by 9,680
- Complexstatement and proof · cited by 5,565
- Norm.normproof · cited by 5,413
- WithTopstatement · cited by 3,754
- absproof · cited by 1,814
- Metric.sphereproof · cited by 371
- Meromorphicstatement and proof · cited by 108
- Real.circleAverageproof · cited by 106
- CircleIntegrableproof · cited by 86
- Real.posLogproof · cited by 61
- Complex.norm_mulproof · cited by 59
Cited by2
Results whose statement or proof uses this declaration.
- ValueDistribution.proximity_mul_zero_leproof · cited by 1
- ValueDistribution.characteristic_mul_top_leproof · cited by 1