Theorems · Theorem · order theory
half_lt_self
∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
0 < a → a / 2 < aAlias of the reverse direction of half_lt_self_iff.
- Defined in
- Mathlib.Algebra.Order.Field.Basic
- Cited by
- 38 results in Mathlib
- Foundations
- Depth 46 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- PartialOrderstatement and proof · cited by 6,410
- IsStrictOrderedRingstatement and proof · cited by 2,490
- Semifieldstatement and proof · cited by 439
- PosMulReflectLTstatement and proof · cited by 278
- half_lt_self_iffproof · cited by 3
Cited by38
Results whose statement or proof uses this declaration.
- Real.sin_pi_div_twoproof · cited by 29
- one_half_lt_oneproof · cited by 12
- Filter.Tendsto.atTop_mul_posproof · cited by 7
- cauchySeq_iff_le_tendsto_0proof · cited by 5
- NNReal.half_lt_selfproof · cited by 4
- PhragmenLindelof.quadrant_Iproof · cited by 4
- ProbabilityTheory.sub_half_inf_sub_mem_Iooproof · cited by 4
- exists_pos_lt_subset_ballproof · cited by 4
- ProbabilityTheory.add_half_inf_sub_mem_Iooproof · cited by 4
- exists_contDiff_tsupport_subsetproof · cited by 3
- ConvexOn.continuousOn_tfaeproof · cited by 3
- TendstoLocallyUniformlyOn.inv₀_of_disjointproof · cited by 3