English
There is a natural bijection between the set of functions f : Ico(0,1) → G and the set of additive maps from R to G with fixed affine term a, namely those of the form R →+c[1, a] G. The bijection is implemented by mkFract.
Русский
Существует естественная биекция между отображениями f : Ico(0,1) → G и отображениями R →+c[1, a] G, задаваемыми фиксированной константой a; биекция задаётся через отображение mkFract.
LaTeX
$$$ (Ico(0,1) \to G) \simeq (R \to+c[1, a] G) $$$$
Lean4
/-- A map `f : R →+c[1, a] G` is defined by its values on `Set.Ico 0 1`. -/
def mkFract : (Ico (0 : R) 1 → G) ≃ (R →+c[1, a] G)
where
toFun
f :=
⟨fun x ↦ f ⟨Int.fract x, Int.fract_nonneg _, Int.fract_lt_one _⟩ + ⌊x⌋ • a, fun x ↦ by
simp [add_one_zsmul, add_assoc]⟩
invFun f x := f x
left_inv _ := by ext x; simp [Int.fract_eq_self.2 x.2, Int.floor_eq_zero_iff.2 x.2]
right_inv f := by ext x; simp [map_fract]
