Theorems · Theorem · order theory
exists_nat_one_div_lt
∀ {K : Type u_4} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {ε : K},
0 < ε → ∃ n, 1 / (↑n + 1) < ε- Defined in
- Mathlib.Algebra.Order.Archimedean.Basic
- Cited by
- 7 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.
Cites9
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
- Archimedeanstatement and proof · cited by 603
- Semifieldstatement and proof · cited by 439
- LT.lt.transproof · cited by 370
- div_lt_iff₀proof · cited by 45
- exists_nat_gtproof · cited by 26
- div_lt_iff₀'proof · cited by 20
- Nat.cast_add_one_posproof · cited by 18
Cited by7
Results whose statement or proof uses this declaration.
- setOfPred_liouvilleWith_subset_auxproof · cited by 2
- AbsolutelyContinuousOnInterval.boundedVariationOnproof · cited by 2
- Metric.uniformity_basis_dist_inv_nat_succproof · cited by 2
- Metric.uniformity_basis_dist_inv_nat_posproof · cited by 1
- MeasureTheory.Measure.exists_positive_of_not_mutuallySingularproof · cited by 1
- Metric.uniformity_basis_dist_le_inv_nat_posproof · cited by 1
- Metric.uniformity_basis_dist_le_inv_nat_succproof · cited by 1