Mathlib Map

Theorems · Theorem · order theory

WithTop.mul_lt_top

∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] [inst_2 : LT α] {a b : WithTop α},
  a < ⊤ → b < ⊤ → a * b < ⊤
Defined in
Mathlib.Algebra.Order.Ring.WithTop
Cited by
4 results in Mathlib
Foundations
Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
DecidableEqMulZeroClassLT
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ENNReal.mul_lt_top · cited by 41ENNReal.mul_lt_topWithTop.prod_lt_top · cited by 2WithTop.prod_lt_topWithBot.bot_lt_mul · cited by 1WithBot.bot_lt_mulSimpleGraph.ediam_eq_top_iff_radius_eq_top · cited by 1SimpleGraph.ediam_eq_top_…Top.top · cited by 9680Top.topWithTop · cited by 3754WithTopMulZeroClass · cited by 232MulZeroClassWithTop.mul_ne_top · cited by 4WithTop.mul_ne_topWithTop.lt_top_iff_ne_top · cited by 3WithTop.lt_top_iff_ne_topWithTop.mul_lt_topCITED BYCITES

Cites5

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.