Mathlib Map

Theorems · Theorem · field theory

Real.sInf_empty

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

gauge_zero · cited by 7gauge_zeroNNReal.coe_sInf · cited by 5NNReal.coe_sInfReal.ediam_eq · cited by 4Real.ediam_eqReal.sInf_smul_of_nonneg · cited by 3Real.sInf_smul_of_nonnegReal.le_sInf · cited by 2Real.le_sInfSeminorm.gauge_ball · cited by 2Seminorm.gauge_ballgauge_empty · cited by 2gauge_emptyReal.sInf_le_sSup · cited by 2Real.sInf_le_sSupNNReal.sInf_empty · cited by 2NNReal.sInf_emptygauge_zero' · cited by 1gauge_zero'NNReal.toReal_limsup · cited by 1NNReal.toReal_limsupReal.iInf_of_isEmpty · cited by 1Real.iInf_of_isEmptyArchimedeanClass.stdPart_eq_sInf · cited by 1ArchimedeanClass.stdPart_…Real.limsSup_of_not_isBounded · cited by 1Real.limsSup_of_not_isBou…gauge_closure_zero · cited by 1gauge_closure_zeroSet · cited by 53352SetReal · cited by 25697RealInfSet.sInf · cited by 935InfSet.sInfneg_zero · cited by 542neg_zeroReal.sSup_empty · cited by 17Real.sSup_emptyReal.sInf_emptyCITED BYCITES

Cites5

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

Cited by21

Results whose statement or proof uses this declaration.