English
For an affine map f: k →ᵃ[k] k and a ≤ b in k with k a field, the image of the closed interval [a,b] under f is the closed interval [f(a), f(b)].
Русский
При отображении f: k →ᵃ[k] k над полем k сохранение замкнутых интервалов: f([a,b]) = [f(a), f(b)].
LaTeX
$$$ f '' \\mathrm{uIcc}(a,b) = \\mathrm{uIcc}(f(a), f(b)) $$$
Lean4
theorem image_uIcc {k : Type*} [Field k] [LinearOrder k] [IsStrictOrderedRing k] (f : k →ᵃ[k] k) (a b : k) :
f '' Set.uIcc a b = Set.uIcc (f a) (f b) :=
by
have : ⇑f = (fun x => x + f 0) ∘ fun x => x * (f 1 - f 0) :=
by
ext x
change f x = x • (f 1 -ᵥ f 0) +ᵥ f 0
rw [← f.linearMap_vsub, ← f.linear.map_smul, ← f.map_vadd]
simp only [vsub_eq_sub, add_zero, mul_one, vadd_eq_add, sub_zero, smul_eq_mul]
rw [this, Set.image_comp]
simp only [Set.image_add_const_uIcc, Set.image_mul_const_uIcc, Function.comp_apply]
