Theorems · Theorem · real analysis
ENNReal.add_ne_top
∀ {a b : ENNReal}, a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤- Defined in
- Mathlib.Data.ENNReal.Operations
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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 · cited by 9,680
- ENNReal.add_lt_topproof · cited by 27
Cited by16
Results whose statement or proof uses this declaration.
- ENNReal.Finiteness.add_ne_topproof · cited by 7
- MeasureTheory.lpNorm_add_leproof · cited by 5
- Metric.hausdorffDist_triangleproof · cited by 2
- MeasureTheory.laverage_union_mem_openSegmentproof · cited by 1
- MeasureTheory.Measure.MeasureDense.of_generateFrom_isSetAlgebra_finiteproof · cited by 1
- MeasureTheory.OuterMeasure.IsMetric.borel_le_caratheodoryproof · cited by 1
- ENNReal.add_rpow_le_rpow_addproof · cited by 1
- MeasureTheory.condExpIndL1Fin_disjoint_unionstatement and proof · cited by 1
- MeasureTheory.SimpleFunc.exists_upperSemicontinuous_le_lintegral_leproof · cited by 1
- MeasureTheory.condExpIndL1_disjoint_unionproof · cited by 1
- MeasureTheory.nonempty_inter_of_measureReal_lt_addproof · cited by 1