Theorems · Theorem · real analysis
Set.OrdConnected.image_real_toNNReal
∀ {s : Set ℝ}, s.OrdConnected → (Real.toNNReal '' s).OrdConnected- Defined in
- Mathlib.Data.NNReal.Defs
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Realstatement and proof · cited by 25,697
- Set.imagestatement · cited by 5,609
- NNRealstatement and proof · cited by 4,310
- Set.Iccproof · cited by 1,702
- NNReal.toRealproof · cited by 1,260
- le_totalproof · cited by 294
- Real.toNNRealstatement and proof · cited by 267
- Set.OrdConnectedstatement and proof · cited by 161
- nonpos_iff_eq_zeroproof · cited by 100
- Set.forall_mem_imageproof · cited by 65
- Set.OrdConnected.outproof · cited by 47
Cited by1
Results whose statement or proof uses this declaration.
- Set.OrdConnected.image_ennreal_ofRealproof · cited by 0