Theorems · Theorem · order theory
Set.uIoc_subset_uIcc
∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.uIoc a b ⊆ Set.uIcc a b- Cited by
- 15 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext
- Assumes
- LinearOrder
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
- LinearOrderstatement and proof · cited by 8,572
- Set.uIccstatement · cited by 393
- Set.uIocstatement · cited by 182
- Set.Ioc_subset_Icc_selfproof · cited by 53
Cited by15
Results whose statement or proof uses this declaration.
- MeromorphicOn.intervalIntegrable_log_normproof · cited by 4
- Frullani.intervalIntegrable_inv_smulproof · cited by 2
- exists_eq_interval_average_of_nullSingletonClassproof · cited by 2
- TendstoUniformlyOn.tendsto_intervalIntegral_of_continuousOnproof · cited by 1
- GaussianFourier.verticalIntegral_norm_leproof · cited by 1
- intervalIntegral.continuous_parametric_primitive_of_continuousproof · cited by 1
- AbsolutelyContinuousOnInterval.integral_deriv_mul_eq_subproof · cited by 1
- LocallyIntegrable.ae_hasDerivAt_integralproof · cited by 1
- exists_eq_const_mul_intervalIntegral_of_ae_nonnegproof · cited by 1
- Frullani.intervalIntegrable_inv_smul_comp_mulproof · cited by 1
- Frullani.norm_integral_inv_smul_sub_leproof · cited by 1
- Frullani.tendsto_integral_inv_smul_atTopproof · cited by 1