Theorems · Theorem · order theory

Nat.mul_lt_floor

∀ {K : Type u_2} [inst : Field K] [inst_1 : LinearOrder K] [IsOrderedRing K] [inst_3 : FloorSemiring K] {a b : K},
  0 < b → b < 1 → ↑⌈b / (1 - b)⌉₊ ≤ a → b * a < ↑⌊a⌋₊

Defined in

Mathlib.Algebra.Order.Floor.Semifield

Cited by

1 results in Mathlib

Foundations

Depth 52 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLinearOrderIsOrderedRingFloorSemiring