Theorems · Theorem · order theory
exists_pos_mul_lt
∀ {α : Type u_4} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α},
0 < a → ∀ (b : α), ∃ c, 0 < c ∧ b * c < a- Defined in
- Mathlib.Algebra.Order.Field.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 45 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LinearOrderstatement and proof · cited by 8,572
- IsStrictOrderedRingstatement and proof · cited by 2,490
- LT.lt.ne'proof · cited by 1,417
- zero_lt_oneproof · cited by 598
- Semifieldstatement and proof · cited by 439
- div_posproof · cited by 337
- lt_add_oneproof · cited by 105
- lt_div_iff₀proof · cited by 44
- lt_max_iffproof · cited by 13
- div_div_cancel₀proof · cited by 5
Cited by13
Results whose statement or proof uses this declaration.
- BoxIntegral.HasIntegral.of_bRiemann_eq_false_of_forall_isLittleOproof · cited by 2
- BoxIntegral.HasIntegral.of_mulproof · cited by 2
- continuousOn_integral_bilinear_of_locally_integrable_of_compact_supportproof · cited by 2
- BoxIntegral.integrable_of_bounded_and_ae_continuousWithinAtproof · cited by 2
- uniformCauchySeqOn_ball_of_fderivproof · cited by 2
- exists_pos_lt_mulproof · cited by 1
- Filter.Tendsto.op_one_isBoundedUnder_le'proof · cited by 1
- BoxIntegral.hasIntegral_GP_pderivproof · cited by 1
- Filter.Tendsto.op_zero_isBoundedUnder_le'proof · cited by 1
- IsTopologicalRing.of_normproof · cited by 0
- TendstoUniformlyOn.tendsto_circleIntegral_of_continuousOnproof · cited by 0
- NormedAddGroupHom.ker_completionproof · cited by 0