English
There are ⌊(b − v) / r⌋ − ⌊(a − v) / r⌋ numbers in Ioc a b that are congruent to v modulo r, i.e., the Nat version of the floor form.
Русский
В интервале Ioc a b ровно ⌊(b − v) / r⌋ − ⌊(a − v) / r⌋ чисел, эквивалентных v по модулю r.
LaTeX
$$$\#\{x \in \mathrm{Ioc}\ a\ b \mid x \equiv v \,[MOD\ r]\} = \max\left( \left\lfloor \frac{b - v}{r} \right\rfloor - \left\lfloor \frac{a - v}{r} \right\rfloor, 0 \right)$$
Lean4
/-- There are `⌊(b - v) / r⌋ - ⌊(a - v) / r⌋` numbers congruent to `v` mod `r` in `(a, b]`,
if `a ≤ b`. `Nat` version of `Int.Ioc_filter_modEq_card`. -/
theorem Ioc_filter_modEq_card (v : ℕ) :
#({x ∈ Ioc a b | x ≡ v [MOD r]}) = max (⌊(b - v) / (r : ℚ)⌋ - ⌊(a - v) / (r : ℚ)⌋) 0 := by
simp_rw [← Ioc_filter_modEq_cast _ _ ▸ card_map _, Int.Ioc_filter_modEq_card _ _ (cast_lt.mpr hr), Int.cast_natCast]
