Mathlib Map

Theorems · Theorem · order theory

WithTop.add_lt_top

∀ {α : Type u} [inst : Add α] {x y : WithTop α} [inst_1 : LT α], x + y < ⊤ ↔ x < ⊤ ∧ y < ⊤
Defined in
Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Cited by
2 results in Mathlib
Foundations
Depth 15 from the axioms · uses propext, Quot.sound
Assumes
AddLT
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ENNReal.add_lt_top · cited by 27ENNReal.add_lt_topENat.add_lt_top · cited by 1ENat.add_lt_topTop.top · cited by 9680Top.topWithTop · cited by 3754WithTopWithTop.add_lt_topCITED BYCITES

Cites2

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

  • Top.topstatement and proof · cited by 9,680
  • WithTopstatement and proof · cited by 3,754

Cited by2

Results whose statement or proof uses this declaration.