Theorems · Theorem · order theory
Set.Ioc_subset_Ioc
∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, b₂ ≤ b₁ → a₁ ≤ a₂ → Set.Ioc b₁ a₁ ⊆ Set.Ioc b₂ a₂- Defined in
- Mathlib.Order.Interval.Set.Basic
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses propext, Quot.sound
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Preorderstatement and proof · cited by 7,952
- Set.Iocstatement and proof · cited by 971
- LE.le.trans'proof · cited by 140
- LT.lt.trans_le'proof · cited by 52
Cited by10
Results whose statement or proof uses this declaration.
- Set.Ioc_subset_Ioc_leftproof · cited by 6
- Finset.Ioc_subset_Iocproof · cited by 3
- BoxIntegral.Box.le_TFAEproof · cited by 2
- Set.Ioc_subset_Ioc_rightproof · cited by 2
- Set.Ioc_subset_uIocproof · cited by 1
- intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le_Icoproof · cited by 1
- intervalIntegral.integral_mono_intervalproof · cited by 1
- Set.uIoc_subset_uIoc_of_uIcc_subset_uIccproof · cited by 1
- BoxIntegral.Box.face_monoproof · cited by 1
- Set.Ioc_subset_uIoc'proof · cited by 0