English
There are exactly those elements x in Ico a b with r | x, given by scaling by r the interval Ico ⌈a/r⌉ ⌈b/r⌉.
Русский
Скаляризация множества x ∈ Ico a b по r даёт ровно множество x ∈ Ico ⌈a/r⌉ ⌈b/r⌉, умноженное на r.
LaTeX
$$$$ \{x\in Ico(a,b)\mid r\mid x\} = (Ico\; \lceil a/r\rceil\; \lceil b/r\rceil).map\langle(\cdot\cdot r), \text{mul_left_injective}_0\; \mathrm{hr.ne'}\rangle.$$$$
Lean4
theorem Ico_filter_dvd_eq :
{x ∈ Ico a b | r ∣ x} = (Ico ⌈a / (r : ℚ)⌉ ⌈b / (r : ℚ)⌉).map ⟨(· * r), mul_left_injective₀ hr.ne'⟩ :=
by
ext x
simp only [mem_map, mem_filter, mem_Ico, ceil_le, lt_ceil, div_le_iff₀, lt_div_iff₀, dvd_iff_exists_eq_mul_left,
cast_pos.2 hr, ← cast_mul, cast_lt, cast_le]
aesop
