Mathlib Map

Theorems · Theorem · number theory

Behrend.ceil_lt_mul

∀ {x : ℝ}, 50 / 19 ≤ x → ↑⌈x⌉₊ < 1.38 * x
Defined in
Mathlib.Combinatorics.Additive.AP.Three.Behrend
Cited by
1 results in Mathlib
Foundations
Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Behrend.bound · cited by 1Behrend.boundReal · cited by 25697RealNat.cast_one · cited by 2501Nat.cast_oneNat.cast_zero · cited by 1870Nat.cast_zeroLT.lt.trans_le · cited by 678lt.trans_lediv_eq_inv_mul · cited by 146div_eq_inv_mulNat.ceil · cited by 141Nat.ceilLE.le.trans' · cited by 140le.trans'le_sub_iff_add_le' · cited by 23le_sub_iff_add_le'one_le_div · cited by 19one_le_divNat.ceil_lt_add_one · cited by 11Nat.ceil_lt_add_onesub_one_mul · cited by 7sub_one_mulBehrend.ceil_lt_mulCITED BYCITES

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.