Theorems · Theorem · general topology

ENNReal.tendsto_toNNReal_iff

∀ {α : Type u_1} {a : ENNReal} {f : α → ENNReal} {u : Filter α},
  a ≠ ⊤ →
    (∀ (x : α), f x ≠ ⊤) → (Filter.Tendsto (ENNReal.toNNReal ∘ f) u (nhds a.toNNReal) ↔ Filter.Tendsto f u (nhds a))

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

ENNRealstatement and proof · cited by 9,879
Top.topstatement and proof · cited by 9,680
Filterstatement and proof · cited by 8,121
nhdsstatement and proof · cited by 5,554
NNRealstatement · cited by 4,310
Filter.Tendstostatement and proof · cited by 3,814
Filter.Tendsto.compproof · cited by 560
ENNReal.toNNRealstatement and proof · cited by 165
ENNReal.tendsto_toNNRealproof · cited by 8
ENNReal.tendsto_coe_toNNRealproof · cited by 1
ENNReal.coe_comp_toNNReal_compproof · cited by 1

Cited by3

Results whose statement or proof uses this declaration.

ENNReal.tendsto_toNNReal_iff'proof · cited by 1
MeasureTheory.tendstoInMeasure_iff_tendsto_toNNRealproof · cited by 1
MeasureTheory.ProbabilityMeasure.exists_lt_measure_biUnion_of_isOpenproof · cited by 1