Theorems · Theorem · real analysis
BoxIntegral.Box.face_mono
∀ {n : ℕ} {I J : BoxIntegral.Box (Fin (n + 1))}, I ≤ J → ∀ (i : Fin (n + 1)), I.face i ≤ J.face i- Defined in
- Mathlib.Analysis.BoxIntegral.Box.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realproof · cited by 25,697
- BoxIntegral.Boxstatement and proof · cited by 464
- Fin.succAboveproof · cited by 249
- BoxIntegral.Box.facestatement and proof · cited by 13
- Set.Ioc_subset_Iocproof · cited by 10
- BoxIntegral.Box.le_iff_boundsproof · cited by 4
Cited by1
Results whose statement or proof uses this declaration.
- BoxIntegral.Box.monotone_faceproof · cited by 0