Ioc_filter_dvd_card — Mathlib

English

There are exactly those x in Ioc a b with r | x, described by a floor-based interval scaled by r and mapped by multiplication by r.

Русский

Количество кратных r в интервале Ioc a b задаётся через отображение на целочисленный интервал, делённый на r и умноженный на r.

LaTeX

$$$$ \{x\in Ioc(a,b)\mid r\mid x\} = (Ioc\; \lfloor a/r\rfloor \; \lfloor b/r\rfloor).map \langle(\cdot\cdot r), \text{mul_left_injective}_0\rangle. $$$$

Lean4

/-- There are `⌊b / r⌋ - ⌊a / r⌋` multiples of `r` in `(a, b]`, if `a ≤ b`. -/
theorem Ioc_filter_dvd_card : #({x ∈ Ioc a b | r ∣ x}) = max (⌊b / (r : ℚ)⌋ - ⌊a / (r : ℚ)⌋) 0 := by
  rw [Ioc_filter_dvd_eq _ _ hr, card_map, card_Ioc, toNat_eq_max]

Похожие утверждения