Theorems · Theorem · general topology

Filter.Tendsto.edist

∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] {f g : β → α} {x : Filter β} {a b : α},
  Filter.Tendsto f x (nhds a) →
    Filter.Tendsto g x (nhds b) → Filter.Tendsto (fun x => edist (f x) (g x)) x (nhds (edist a b))

Defined in: Mathlib.Topology.Instances.ENNReal.Lemmas
Cited by: 3 results in Mathlib
Foundations: Depth 149 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: PseudoEMetricSpace

Mathlib docs Source Loogle LeanSearch

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.

ENNRealstatement · cited by 9,879
Filterstatement and proof · cited by 8,121
nhdsstatement and proof · cited by 5,554
Filter.Tendstostatement and proof · cited by 3,814
PseudoEMetricSpacestatement and proof · cited by 1,536
EDist.ediststatement · cited by 735
Filter.Tendsto.compproof · cited by 560
Continuous.tendstoproof · cited by 206
Filter.Tendsto.prodMk_nhdsproof · cited by 46
continuous_edistproof · cited by 9

Cited by3

Results whose statement or proof uses this declaration.

eVariationOn.eVariationOn_on_inter_Iic_eq_Iio_add_edistproof · cited by 4
edist_le_tsum_of_edist_le_of_tendstoproof · cited by 2
eVariationOn.lowerSemicontinuous_auxproof · cited by 2