Theorem: ContinuousMultilinearMap.eq_empty (ForML/ContinuousMultilinearMap.lean)

State before:
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : IsEmpty ι
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_5
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : ContinuousMultilinearMap 𝕜 E G
⊢ c = constOfIsEmpty 𝕜 E (c 0)
Tactic:
ext m
State after:
case H
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : IsEmpty ι
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_5
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ c m = (constOfIsEmpty 𝕜 E (c 0)) m

State before:
case H
ι : Type u_1
inst✝⁸ : Fintype ι
inst✝⁷ : IsEmpty ι
𝕜 : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_5
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ c m = (constOfIsEmpty 𝕜 E (c 0)) m
Tactic:
simp [Subsingleton.elim m 0]
State after:
no goals