Mathlib Map

Theorems · Theorem · real analysis

ENNReal.top_rpow_of_neg

∀ {y : ℝ}, y < 0 → ⊤ ^ y = 0
Defined in
Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Cited by
12 results in Mathlib
Foundations
Depth 200 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.

ENNReal.rpow_mul · cited by 33ENNReal.rpow_mulENNReal.rpow_neg · cited by 6ENNReal.rpow_negENNReal.mul_rpow_eq_ite · cited by 5ENNReal.mul_rpow_eq_iteENNReal.log_rpow · cited by 4ENNReal.log_rpowENNReal.inv_rpow · cited by 3ENNReal.inv_rpowENNReal.toNNReal_rpow · cited by 2ENNReal.toNNReal_rpowENNReal.rpow_eq_top_iff · cited by 1ENNReal.rpow_eq_top_iffENNReal.rpow_le_rpow_of_exponent_le · cited by 1ENNReal.rpow_le_rpow_of_e…MeasureTheory.eLpNorm'_zero' · cited by 1MeasureTheory.eLpNorm'_ze…ENNReal.rpow_lt_one_of_one_lt_of_neg · cited by 0ENNReal.rpow_lt_one_of_on…ENNReal.rpow_eq_zero_iff · cited by 0ENNReal.rpow_eq_zero_iffENNReal.rpow_le_one_of_one_le_of_neg · cited by 0ENNReal.rpow_le_one_of_on…Real · cited by 25697RealENNReal · cited by 9879ENNRealTop.top · cited by 9680Top.topne_of_lt · cited by 203ne_of_ltasymm · cited by 12asymmENNReal.top_rpow_of_negCITED BYCITES

Cites5

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

  • Realstatement and proof · cited by 25,697
  • ENNRealstatement · cited by 9,879
  • Top.topstatement and proof · cited by 9,680
  • ne_of_ltproof · cited by 203
  • asymmproof · cited by 12

Cited by12

Results whose statement or proof uses this declaration.