Mathlib Map

Theorems · Theorem · general topology

EReal.continuous_toENNReal

Continuous EReal.toENNReal
Defined in
Mathlib.Topology.Instances.EReal.Lemmas
Cited by
4 results in Mathlib
Foundations
Depth 132 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Continuous.ereal_toENNReal · cited by 0Continuous.ereal_toENNRealContinuousWithinAt.ereal_toENNReal · cited by 0ContinuousWithinAt.ereal_…ContinuousOn.ereal_toENNReal · cited by 0ContinuousOn.ereal_toENNR…ContinuousAt.ereal_toENNReal · cited by 0ContinuousAt.ereal_toENNR…Real · cited by 25697RealENNReal · cited by 9879ENNRealTop.top · cited by 9680Top.topnhds · cited by 5554nhdsBot.bot · cited by 4720Bot.botFilter.Tendsto · cited by 3814Filter.TendstoFilter.Eventually · cited by 3134Filter.EventuallyCompl.compl · cited by 2925Compl.complContinuous · cited by 2592ContinuousLT.lt.le · cited by 2189lt.leFilter.univ_mem' · cited by 1672Filter.univ_mem'Filter.mp_mem · cited by 1537Filter.mp_memENNReal.ofReal · cited by 863ENNReal.ofRealEReal · cited by 793ERealReal.toEReal · cited by 303Real.toERealEReal.continuous_toENNRealCITED BYCITES

Cites41

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

Cited by4

Results whose statement or proof uses this declaration.