Ico_filter_dvd_card — Mathlib

English

The number of multiples of r in Ioc a b equals max(⌊b/r⌋ − ⌊a/r⌋, 0).

Русский

Количество кратных r в интервале Ioc a b равно max(⌊b/r⌋ − ⌊a/r⌋, 0).

LaTeX

$$$$ \#\{x\in Ioc(a,b)\mid r\mid x\} = \max\big(\lfloor b/r\rfloor - \lfloor a/r\rfloor, 0\big). $$$$

Lean4

/-- There are `⌈b / r⌉ - ⌈a / r⌉` multiples of `r` in `[a, b)`, if `a ≤ b`. -/
theorem Ico_filter_dvd_card : #({x ∈ Ico a b | r ∣ x}) = max (⌈b / (r : ℚ)⌉ - ⌈a / (r : ℚ)⌉) 0 := by
  rw [Ico_filter_dvd_eq _ _ hr, card_map, card_Ico, toNat_eq_max]

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