Mathlib Map

Theorems · Definition · general topology

unitInterval.toNNReal

↑unitInterval → NNReal

The coercion from I to ℝ≥0.

Defined in
Mathlib.Topology.UnitInterval
Cited by
34 results in Mathlib
Foundations
Depth 104 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.

ProbabilityTheory.bernoulliMeasure · cited by 19ProbabilityTheory.bernoul…ProbabilityTheory.setBernoulli · cited by 19ProbabilityTheory.setBern…ProbabilityTheory.bernoulliMeasure_apply · cited by 5ProbabilityTheory.bernoul…ProbabilityTheory.setBernoulli_ae_subset · cited by 5ProbabilityTheory.setBern…ProbabilityTheory.bernoulliMeasure_real_apply · cited by 4ProbabilityTheory.bernoul…ProbabilityTheory.setBernoulli_singleton · cited by 3ProbabilityTheory.setBern…unitInterval.toNNReal_add_toNNReal_symm · cited by 3unitInterval.toNNReal_add…ProbabilityTheory.setBernoulli_apply · cited by 2ProbabilityTheory.setBern…ProbabilityTheory.setBernoulli_empty · cited by 2ProbabilityTheory.setBern…ProbabilityTheory.setBernoulli_eq_map · cited by 2ProbabilityTheory.setBern…ProbabilityTheory.bernoulliMeasure_def · cited by 1ProbabilityTheory.bernoul…ProbabilityTheory.bernoulliMeasure_real_apply_of_mem_of_notMem · cited by 1ProbabilityTheory.bernoul…ProbabilityTheory.bernoulliMeasure_real_apply_of_notMem_of_mem · cited by 1ProbabilityTheory.bernoul…ProbabilityTheory.bernoulliMeasure_real_apply_of_notMem_of_notMem · cited by 1ProbabilityTheory.bernoul…ProbabilityTheory.setBernoulli_apply' · cited by 1ProbabilityTheory.setBern…Real · cited by 25697RealSet.Elem · cited by 7166Set.ElemNNReal · cited by 4310NNRealunitInterval · cited by 607unitIntervalunitInterval.toNNRealCITED BYCITES

Cites4

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

  • Realstatement · cited by 25,697
  • Set.Elemstatement and proof · cited by 7,166
  • NNRealstatement · cited by 4,310
  • unitIntervalstatement and proof · cited by 607

Cited by36

Results whose statement or proof uses this declaration.