R : Type u_2
E : Type ?u.12383
F : Type u_1
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
R : Type u_2
E : Type ?u.12383
F : Type u_1
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)
suffices ⇑(homothety x t) = fun y => t • (y - x) + x by
  rw [this]
  exact ((continuous_id.sub continuous_const).const_smul _).add continuous_const
case h
R : Type u_2
E : Type ?u.12383
F : Type u_1
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
R : Type u_2
E : Type ?u.12383
F : Type u_1
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
ext y
no goals
case h
R : Type u_2
E : Type ?u.12383
F : Type u_1
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
simp [homothety_apply]
R : Type u_2
E : Type ?u.12383
F : Type u_1
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
R : Type u_2
E : Type ?u.12383
F : Type u_1
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)
rw [this]
no goals
R : Type u_2
E : Type ?u.12383
F : Type u_1
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
exact ((continuous_id.sub continuous_const).const_smul _).add continuous_const