[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
⊢ Continuous ↑f ↔ Continuous ↑f.linear
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
⊢ Continuous ↑f → Continuous ↑f.linear
[PROOFSTEP]
intro hc
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
hc : Continuous ↑f
⊢ Continuous ↑f.linear
[PROOFSTEP]
rw [decomp' f]
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
hc : Continuous ↑f
⊢ Continuous (↑f - fun x => ↑f 0)
[PROOFSTEP]
exact hc.sub continuous_const
[GOAL]
case mpr
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
⊢ Continuous ↑f.linear → Continuous ↑f
[PROOFSTEP]
intro hc
[GOAL]
case mpr
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
hc : Continuous ↑f.linear
⊢ Continuous ↑f
[PROOFSTEP]
rw [decomp f]
[GOAL]
case mpr
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
hc : Continuous ↑f.linear
⊢ Continuous (↑f.linear + fun x => ↑f 0)
[PROOFSTEP]
exact hc.add continuous_const
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : CommRing R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
⊢ Continuous ↑(homothety x t)
[PROOFSTEP]
suffices ⇑(homothety x t) = fun y => t • (y - x) + x by
  rw [this]
  exact ((continuous_id.sub continuous_const).const_smul _).add continuous_const
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : CommRing R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
this : ↑(homothety x t) = fun y => t • (y - x) + x
⊢ Continuous ↑(homothety x t)
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : CommRing R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
this : ↑(homothety x t) = fun y => t • (y - x) + x
⊢ Continuous fun y => t • (y - x) + x
[PROOFSTEP]
exact ((continuous_id.sub continuous_const).const_smul _).add continuous_const
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : CommRing R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
⊢ ↑(homothety x t) = fun y => t • (y - x) + x
[PROOFSTEP]
ext y
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : CommRing R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
y : F
⊢ ↑(homothety x t) y = t • (y - x) + x
[PROOFSTEP]
simp [homothety_apply]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Field R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
ht : t ≠ 0
⊢ IsOpenMap ↑(homothety x t)
[PROOFSTEP]
apply IsOpenMap.of_inverse (homothety_continuous x t⁻¹)
[GOAL]
case l_inv
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Field R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
ht : t ≠ 0
⊢ Function.LeftInverse ↑(homothety x t) ↑(homothety x t⁻¹)
[PROOFSTEP]
intro e
[GOAL]
case r_inv
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Field R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
ht : t ≠ 0
⊢ Function.RightInverse ↑(homothety x t) ↑(homothety x t⁻¹)
[PROOFSTEP]
intro e
[GOAL]
case l_inv
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Field R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
ht : t ≠ 0
e : F
⊢ ↑(homothety x t) (↑(homothety x t⁻¹) e) = e
[PROOFSTEP]
simp [← AffineMap.comp_apply, ← homothety_mul, ht]
[GOAL]
case r_inv
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Field R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
ht : t ≠ 0
e : F
⊢ ↑(homothety x t⁻¹) (↑(homothety x t) e) = e
[PROOFSTEP]
simp [← AffineMap.comp_apply, ← homothety_mul, ht]
