Mathlib Map

Theorems · Theorem · order theory

ENat.sSup_eq_zero

∀ {s : Set ℕ∞}, sSup s = 0 ↔ ∀ a ∈ s, a = 0
Defined in
Mathlib.Data.ENat.Lattice
Cited by
0 results in Mathlib
Foundations
Depth 32 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.

Set · cited by 53352SetENat · cited by 4985ENatSupSet.sSup · cited by 954SupSet.sSupsSup_eq_bot · cited by 7sSup_eq_botENat.sSup_eq_zeroCITED BYCITES

Cites4

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

  • Setstatement and proof · cited by 53,352
  • ENatstatement and proof · cited by 4,985
  • SupSet.sSupstatement · cited by 954
  • sSup_eq_botproof · cited by 7

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.