Mathlib Map

Theorems · Theorem · real analysis

BoxIntegral.unitPartition.diam_boxIcc

∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] [inst_1 : Fintype ι] (ν : ι → ℤ),
  Metric.diam (BoxIntegral.Box.Icc (BoxIntegral.unitPartition.box n ν)) ≤ 1 / ↑n
Defined in
Mathlib.Analysis.BoxIntegral.UnitPartition
Cited by
1 results in Mathlib
Foundations
Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
NeZeroFintype
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

BoxIntegral.unitPartition.prepartition_isSubordinate · cited by 1unitPartition.prepartitio…DFunLike.coe · cited by 62936DFunLike.coeSet · cited by 53352SetReal · cited by 25697RealFintype · cited by 7736FintypeNat.cast_one · cited by 2501Nat.cast_oneENNReal.ofReal · cited by 863ENNReal.ofRealOrderEmbedding · cited by 619OrderEmbeddingBoxIntegral.Box · cited by 464BoxIntegral.BoxNat.cast_nonneg' · cited by 245Nat.cast_nonneg'BoxIntegral.Box.Icc · cited by 76Box.IccMetric.diam · cited by 74Metric.diamBoxIntegral.Box.upper · cited by 70Box.upperBoxIntegral.Box.lower · cited by 65Box.lowerMathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg · cited by 29Positivity.div_nonneg_of_…BoxIntegral.unitPartition.box · cited by 22unitPartition.boxunitPartition.diam_boxIccCITED BYCITES

Cites20

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

Cited by1

Results whose statement or proof uses this declaration.