Mathlib Map

Theorems · Theorem · order theory

WithTop.sub_ne_top_iff

∀ {α : Type u_1} [inst : Sub α] [inst_1 : Bot α] {a b : WithTop α}, a - b ≠ ⊤ ↔ a ≠ ⊤ ∨ b = ⊤
Defined in
Mathlib.Algebra.Order.Sub.WithTop
Cited by
2 results in Mathlib
Foundations
Depth 15 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
SubBot
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ENNReal.sub_ne_top_iff · cited by 0ENNReal.sub_ne_top_iffENat.sub_ne_top_iff · cited by 0ENat.sub_ne_top_iffTop.top · cited by 9680Top.topWithTop · cited by 3754WithTopBot · cited by 96BotWithTop.sub_ne_top_iffCITED BYCITES

Cites3

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
  • Botstatement and proof · cited by 96

Cited by2

Results whose statement or proof uses this declaration.