R₁ : Type u_1
R₂ : Type u_2
R₃ : Type ?u.448146
inst✝¹⁶ : Semiring R₁
inst✝¹⁵ : Semiring R₂
inst✝¹⁴ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_3
inst✝¹³ : TopologicalSpace M₁
inst✝¹² : AddCommMonoid M₁
M'₁ : Type ?u.448233
inst✝¹¹ : TopologicalSpace M'₁
inst✝¹⁰ : AddCommMonoid M'₁
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
M₃ : Type ?u.448251
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
M₄ : Type ?u.448260
inst✝⁵ : TopologicalSpace M₄
inst✝⁴ : AddCommMonoid M₄
inst✝³ : Module R₁ M₁
inst✝² : Module R₁ M'₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
f : M₁ →SL[σ₁₂] M₂
hf : f ≠ 0
h : ∀ (x : M₁), ↑f x = 0
⊢ False
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type ?u.448146
inst✝¹⁶ : Semiring R₁
inst✝¹⁵ : Semiring R₂
inst✝¹⁴ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_3
inst✝¹³ : TopologicalSpace M₁
inst✝¹² : AddCommMonoid M₁
M'₁ : Type ?u.448233
inst✝¹¹ : TopologicalSpace M'₁
inst✝¹⁰ : AddCommMonoid M'₁
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
M₃ : Type ?u.448251
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
M₄ : Type ?u.448260
inst✝⁵ : TopologicalSpace M₄
inst✝⁴ : AddCommMonoid M₄
inst✝³ : Module R₁ M₁
inst✝² : Module R₁ M'₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
f : M₁ →SL[σ₁₂] M₂
hf : f ≠ 0
⊢ ∃ x, ↑f x ≠ 0
by_contra' h
no goals
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type ?u.448146
inst✝¹⁶ : Semiring R₁
inst✝¹⁵ : Semiring R₂
inst✝¹⁴ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_3
inst✝¹³ : TopologicalSpace M₁
inst✝¹² : AddCommMonoid M₁
M'₁ : Type ?u.448233
inst✝¹¹ : TopologicalSpace M'₁
inst✝¹⁰ : AddCommMonoid M'₁
M₂ : Type u_4
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
M₃ : Type ?u.448251
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
M₄ : Type ?u.448260
inst✝⁵ : TopologicalSpace M₄
inst✝⁴ : AddCommMonoid M₄
inst✝³ : Module R₁ M₁
inst✝² : Module R₁ M'₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
f : M₁ →SL[σ₁₂] M₂
hf : f ≠ 0
h : ∀ (x : M₁), ↑f x = 0
⊢ False
exact hf (ContinuousLinearMap.ext h)