English
The preimage of a set s under fract equals the union over all integers m of the preimage under x ↦ x − m of s ∩ [0,1).
Русский
Обратное изображение множества s под fract равно объединению по всем целым m множеств, взятых как (x ↦ x − m)^{-1}(s ∩ [0,1)).
LaTeX
$$$\\\\operatorname{fract}^{-1}(s) = \\\\bigcup_{m \\\\in \\\\mathbb{Z}} (x \\\\mapsto x - m)^{-1} ( s \\cap Ico(0,1) )$$$
Lean4
theorem preimage_fract (s : Set R) : fract ⁻¹' s = ⋃ m : ℤ, (fun x => x - (m : R)) ⁻¹' (s ∩ Ico (0 : R) 1) :=
by
ext x
simp only [mem_preimage, mem_iUnion, mem_inter_iff]
refine ⟨fun h => ⟨⌊x⌋, h, fract_nonneg x, fract_lt_one x⟩, ?_⟩
rintro ⟨m, hms, hm0, hm1⟩
obtain rfl : ⌊x⌋ = m := floor_eq_iff.2 ⟨sub_nonneg.1 hm0, sub_lt_iff_lt_add'.1 hm1⟩
exact hms
