Mathlib Map

Theorems · Theorem · field theory

Real.sSup_empty

sSup ∅ = 0
Defined in
Mathlib.Algebra.Order.Archimedean.Real.Basic
Cited by
17 results in Mathlib
Foundations
Depth 113 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.

Real.sInf_empty · cited by 21Real.sInf_emptyReal.iSup_of_isEmpty · cited by 14Real.iSup_of_isEmptyNNReal.coe_sSup · cited by 5NNReal.coe_sSupReal.ediam_eq · cited by 4Real.ediam_eqReal.sSup_nonneg · cited by 4Real.sSup_nonnegMvPowerSeries.gaussNorm_nonneg · cited by 3MvPowerSeries.gaussNorm_n…BoundedContinuousFunction.dist_eq_iSup · cited by 3BoundedContinuousFunction…Real.sInf_le_sSup · cited by 2Real.sInf_le_sSupReal.sSup_le · cited by 2Real.sSup_leAsymptotics.IsBigOWith.sum_congr · cited by 1IsBigOWith.sum_congrVitali.exists_disjoint_covering_ae · cited by 1Vitali.exists_disjoint_co…Real.limsInf_of_not_isBounded · cited by 1Real.limsInf_of_not_isBou…Real.sInf_smul_of_nonpos · cited by 1Real.sInf_smul_of_nonposReal.sInf_univ · cited by 1Real.sInf_univReal.sSup_neg · cited by 1Real.sSup_negSet · cited by 53352SetReal · cited by 25697RealSupSet.sSup · cited by 954SupSet.sSupReal.sSup_emptyCITED BYCITES

Cites3

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

  • Setstatement · cited by 53,352
  • Realstatement · cited by 25,697
  • SupSet.sSupstatement · cited by 954

Cited by17

Results whose statement or proof uses this declaration.