Theorems · Theorem · complex analysis

ValueDistribution.proximity_congr_codiscreteWithin

∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f g : ℂ → E} {a : WithTop E} {r : ℝ},
  f =ᶠ[Filter.codiscreteWithin (Metric.sphere 0 |r|)] g →
    r ≠ 0 → ValueDistribution.proximity f a r = ValueDistribution.proximity g a r

If two functions differ only on a discrete set, then their proximity functions agree, except perhaps at radius 0.

Defined in

Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Cited by

1 results in Mathlib

Foundations

Depth 258 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroup