Theorems · Theorem · probability
ProbabilityTheory.sub_half_inf_sub_mem_Ioo
∀ {l u v : ℝ}, v ∈ Set.Ioo l u → v - min (v - l) (u - v) / 2 ∈ Set.Ioo l u- Cited by
- 4 results in Mathlib
- Foundations
- Depth 106 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Realstatement and proof · cited by 25,697
- Set.Ioostatement and proof · cited by 1,214
- le_of_ltproof · cited by 1,175
- div_posproof · cited by 337
- inf_le_leftproof · cited by 286
- le_add_of_nonneg_rightproof · cited by 69
- sub_le_iff_le_addproof · cited by 50
- sub_le_sub_leftproof · cited by 43
- half_lt_selfproof · cited by 38
- sub_lt_sub_leftproof · cited by 9
Cited by4
Results whose statement or proof uses this declaration.
- ProbabilityTheory.aemeasurable_of_mem_interior_integrableExpSetproof · cited by 6
- ProbabilityTheory.hasDerivAt_integral_pow_mul_expproof · cited by 3