Theorems · Theorem · order theory
Set.uIcc_of_le
∀ {α : Type u_1} [inst : Lattice α] {a b : α}, a ≤ b → Set.uIcc a b = Set.Icc a b- Cited by
- 54 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses propext
- Assumes
- Lattice
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.
- Setstatement and proof · cited by 53,352
- Set.Iccstatement and proof · cited by 1,702
- Latticestatement and proof · cited by 916
- Set.uIccstatement · cited by 393
- sup_eq_rightproof · cited by 53
- inf_eq_leftproof · cited by 41
Cited by54
Results whose statement or proof uses this declaration.
- intervalIntegral.integral_eq_sub_of_hasDeriv_rightproof · cited by 8
- Set.uIcc_of_ltproof · cited by 5
- ContinuousOn.intervalIntegrable_of_Iccproof · cited by 5
- intervalIntegral.integral_deriv_smul_comp'''proof · cited by 4
- Module.Basis.parallelepiped_basisFunproof · cited by 3
- intermediate_value_uIccproof · cited by 3
- Set.image_mul_const_uIccproof · cited by 3
- curveIntegral_segmentproof · cited by 2
- MeasureTheory.integral_deriv_smul_comp_Ioiproof · cited by 2
- ContinuousOn.image_uIccproof · cited by 2
- intervalIntegral.integral_unitInterval_deriv_eq_subproof · cited by 2
- MeasureTheory.tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioiproof · cited by 2