English
The image of a set s under fract equals the union over integers m of ((x − m) applied to s) ∩ [0,1).
Русский
Образ множества s под fract равен объединению по целым m: (x − m)''s ∩ [0,1).
LaTeX
$$$\\\\operatorname{fract}'' s = \\\\bigcup_{m \\\\in \\\\mathbb{Z}} ( x \\\\mapsto x - m) '' s \\\\cap Ico(0,1)$$$
Lean4
theorem image_fract (s : Set R) : fract '' s = ⋃ m : ℤ, (fun x : R => x - m) '' s ∩ Ico 0 1 :=
by
ext x
simp only [mem_image, mem_inter_iff, mem_iUnion]; constructor
· rintro ⟨y, hy, rfl⟩
exact ⟨⌊y⌋, ⟨y, hy, rfl⟩, fract_nonneg y, fract_lt_one y⟩
· rintro ⟨m, ⟨y, hys, rfl⟩, h0, h1⟩
obtain rfl : ⌊y⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 h0, sub_lt_iff_lt_add'.1 h1⟩
exact ⟨y, hys, rfl⟩
