no goals
R : Type u_1
M : Type u_2
inst✝⁷ : TopologicalSpace R
inst✝⁶ : DivisionRing R
inst✝⁵ : ContinuousSub R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
f : M →L[R] R
hf : f ≠ 0
x : M
hx : ↑f x ≠ 0
y : M
⊢ Continuous fun a => y + (a - ↑f y) • (↑f x)⁻¹ • x
continuity
no goals
R : Type u_1
M : Type u_2
inst✝⁷ : TopologicalSpace R
inst✝⁶ : DivisionRing R
inst✝⁵ : ContinuousSub R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
f : M →L[R] R
hf : f ≠ 0
x : M
hx : ↑f x ≠ 0
y : M
⊢ (fun a => y + (a - ↑f y) • (↑f x)⁻¹ • x) (↑f y) = y
simp
no goals
R : Type u_1
M : Type u_2
inst✝⁷ : TopologicalSpace R
inst✝⁶ : DivisionRing R
inst✝⁵ : ContinuousSub R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
f : M →L[R] R
hf : f ≠ 0
x : M
hx : ↑f x ≠ 0
y : M
a : R
⊢ ↑f ((fun a => y + (a - ↑f y) • (↑f x)⁻¹ • x) a) = a
simp [hx]