Ioc_filter_dvd_eq — Mathlib

English

The number of multiples of r in Ico a b equals max(⌈b/r⌉ − ⌈a/r⌉, 0).

Русский

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

LaTeX

$$$$ \#\{x\in Ico(a,b)\mid r\mid x\} = \max\big(\lceil b/r\rceil - \lceil a/r\rceil, 0\big). $$$$

Lean4

theorem Ioc_filter_dvd_eq :
    {x ∈ Ioc a b | r ∣ x} = (Ioc ⌊a / (r : ℚ)⌋ ⌊b / (r : ℚ)⌋).map ⟨(· * r), mul_left_injective₀ hr.ne'⟩ :=
  by
  ext x
  simp only [mem_map, mem_filter, mem_Ioc, floor_lt, le_floor, div_lt_iff₀, le_div_iff₀, dvd_iff_exists_eq_mul_left,
    cast_pos.2 hr, ← cast_mul, cast_lt, cast_le]
  aesop

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