Theorem: Fin.cons.norm (ForML/ContinuousMultilinearMap.lean)

State before:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ
E : Fin n → Type u_2
inst✝⁶ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁵ : (i : Fin n) → NormedSpace 𝕜 (E i)
E₁ : Fin n → Type u_3
inst✝⁴ : (i : Fin n) → NormedAddCommGroup (E₁ i)
inst✝³ : (i : Fin n) → NormedSpace 𝕜 (E₁ i)
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
α : Fin (Nat.succ n) → Type u_5
inst✝ : (i : Fin (Nat.succ n)) → SeminormedAddGroup (α i)
a : α 0
b : (i : Fin n) → α (succ i)
⊢ ‖cons a b‖ = ‖a‖ ⊔ ‖b‖
Tactic:
rw [← Real.toNNReal_eq_toNNReal_iff]
State after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ
E : Fin n → Type u_2
inst✝⁶ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁵ : (i : Fin n) → NormedSpace 𝕜 (E i)
E₁ : Fin n → Type u_3
inst✝⁴ : (i : Fin n) → NormedAddCommGroup (E₁ i)
inst✝³ : (i : Fin n) → NormedSpace 𝕜 (E₁ i)
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
α : Fin (Nat.succ n) → Type u_5
inst✝ : (i : Fin (Nat.succ n)) → SeminormedAddGroup (α i)
a : α 0
b : (i : Fin n) → α (succ i)
⊢ Real.toNNReal ‖cons a b‖ = Real.toNNReal (‖a‖ ⊔ ‖b‖)

case hr
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ
E : Fin n → Type u_2
inst✝⁶ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁵ : (i : Fin n) → NormedSpace 𝕜 (E i)
E₁ : Fin n → Type u_3
inst✝⁴ : (i : Fin n) → NormedAddCommGroup (E₁ i)
inst✝³ : (i : Fin n) → NormedSpace 𝕜 (E₁ i)
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
α : Fin (Nat.succ n) → Type u_5
inst✝ : (i : Fin (Nat.succ n)) → SeminormedAddGroup (α i)
a : α 0
b : (i : Fin n) → α (succ i)
⊢ 0 ≤ ‖cons a b‖

case hp
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ
E : Fin n → Type u_2
inst✝⁶ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁵ : (i : Fin n) → NormedSpace 𝕜 (E i)
E₁ : Fin n → Type u_3
inst✝⁴ : (i : Fin n) → NormedAddCommGroup (E₁ i)
inst✝³ : (i : Fin n) → NormedSpace 𝕜 (E₁ i)
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
α : Fin (Nat.succ n) → Type u_5
inst✝ : (i : Fin (Nat.succ n)) → SeminormedAddGroup (α i)
a : α 0
b : (i : Fin n) → α (succ i)
⊢ 0 ≤ ‖a‖ ⊔ ‖b‖

State before:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ
E : Fin n → Type u_2
inst✝⁶ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁵ : (i : Fin n) → NormedSpace 𝕜 (E i)
E₁ : Fin n → Type u_3
inst✝⁴ : (i : Fin n) → NormedAddCommGroup (E₁ i)
inst✝³ : (i : Fin n) → NormedSpace 𝕜 (E₁ i)
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
α : Fin (Nat.succ n) → Type u_5
inst✝ : (i : Fin (Nat.succ n)) → SeminormedAddGroup (α i)
a : α 0
b : (i : Fin n) → α (succ i)
⊢ Real.toNNReal ‖cons a b‖ = Real.toNNReal (‖a‖ ⊔ ‖b‖)
Tactic:
rw [Real.toNNReal_mono.map_sup]
State after:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ
E : Fin n → Type u_2
inst✝⁶ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁵ : (i : Fin n) → NormedSpace 𝕜 (E i)
E₁ : Fin n → Type u_3
inst✝⁴ : (i : Fin n) → NormedAddCommGroup (E₁ i)
inst✝³ : (i : Fin n) → NormedSpace 𝕜 (E₁ i)
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
α : Fin (Nat.succ n) → Type u_5
inst✝ : (i : Fin (Nat.succ n)) → SeminormedAddGroup (α i)
a : α 0
b : (i : Fin n) → α (succ i)
⊢ Real.toNNReal ‖cons a b‖ = Real.toNNReal ‖a‖ ⊔ Real.toNNReal ‖b‖

State before:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ
E : Fin n → Type u_2
inst✝⁶ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁵ : (i : Fin n) → NormedSpace 𝕜 (E i)
E₁ : Fin n → Type u_3
inst✝⁴ : (i : Fin n) → NormedAddCommGroup (E₁ i)
inst✝³ : (i : Fin n) → NormedSpace 𝕜 (E₁ i)
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
α : Fin (Nat.succ n) → Type u_5
inst✝ : (i : Fin (Nat.succ n)) → SeminormedAddGroup (α i)
a : α 0
b : (i : Fin n) → α (succ i)
⊢ Real.toNNReal ‖cons a b‖ = Real.toNNReal ‖a‖ ⊔ Real.toNNReal ‖b‖
Tactic:
simpa [norm_toNNReal] using nnnorm a b
State after:
no goals

State before:
case hr
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ
E : Fin n → Type u_2
inst✝⁶ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁵ : (i : Fin n) → NormedSpace 𝕜 (E i)
E₁ : Fin n → Type u_3
inst✝⁴ : (i : Fin n) → NormedAddCommGroup (E₁ i)
inst✝³ : (i : Fin n) → NormedSpace 𝕜 (E₁ i)
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
α : Fin (Nat.succ n) → Type u_5
inst✝ : (i : Fin (Nat.succ n)) → SeminormedAddGroup (α i)
a : α 0
b : (i : Fin n) → α (succ i)
⊢ 0 ≤ ‖cons a b‖
Tactic:
exact norm_nonneg (cons a b)
State after:
no goals

State before:
case hp
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
n : ℕ
E : Fin n → Type u_2
inst✝⁶ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁵ : (i : Fin n) → NormedSpace 𝕜 (E i)
E₁ : Fin n → Type u_3
inst✝⁴ : (i : Fin n) → NormedAddCommGroup (E₁ i)
inst✝³ : (i : Fin n) → NormedSpace 𝕜 (E₁ i)
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
α : Fin (Nat.succ n) → Type u_5
inst✝ : (i : Fin (Nat.succ n)) → SeminormedAddGroup (α i)
a : α 0
b : (i : Fin n) → α (succ i)
⊢ 0 ≤ ‖a‖ ⊔ ‖b‖
Tactic:
exact le_trans (norm_nonneg a) le_sup_left
State after:
no goals