internlm/Lean-Github huggingface dataset:
Theorem: Fin.map_cons'
Proof state before:
case h
𝕜 : 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
α : Type u_5
δ₁ : Type u_6
n : ℕ
f : Fin (Nat.succ n) → α → δ₁
x : α
p : Fin n → α
i : Fin (Nat.succ n)
⊢ f i (cons x p i) = cons (f 0 x) (fun i => f (succ i) (p i)) i
Tactic:
cases i using Fin.cases <;> simp
Proof state after:
no goals
Theorem: Fin.map_cons
Proof 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
n : ℕ
α : Fin (Nat.succ n) → Type u_5
δ₁ : Fin (Nat.succ n) → Type u_6
f : (i : Fin (Nat.succ n)) → α i → δ₁ i
x : α 0
p : (i : Fin n) → α (succ i)
⊢ (fun i => f i (cons x p i)) = cons (f 0 x) fun i => f (succ i) (p i)
Tactic:
ext i
Proof state after:
case h
𝕜 : 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
n : ℕ
α : Fin (Nat.succ n) → Type u_5
δ₁ : Fin (Nat.succ n) → Type u_6
f : (i : Fin (Nat.succ n)) → α i → δ₁ i
x : α 0
p : (i : Fin n) → α (succ i)
i : Fin (Nat.succ n)
⊢ f i (cons x p i) = cons (f 0 x) (fun i => f (succ i) (p i)) i
Theorem: Fin.map_cons
Proof state before:
case h
𝕜 : 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
n : ℕ
α : Fin (Nat.succ n) → Type u_5
δ₁ : Fin (Nat.succ n) → Type u_6
f : (i : Fin (Nat.succ n)) → α i → δ₁ i
x : α 0
p : (i : Fin n) → α (succ i)
i : Fin (Nat.succ n)
⊢ f i (cons x p i) = cons (f 0 x) (fun i => f (succ i) (p i)) i
Tactic:
cases i using Fin.cases <;> simp
Proof state after:
no goals
Theorem: Fin.cons.nnnorm
Proof 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:
simp [Pi.nnnorm_def, Fin.univ_succ, Function.comp_def]
Proof state after:
no goals
Theorem: Fin.cons.norm
Proof 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]
Proof 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‖
Theorem: Fin.cons.norm
Proof 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]
Proof 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‖
Theorem: Fin.cons.norm
Proof 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
Proof state after:
no goals
Theorem: Fin.cons.norm
Proof 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)
Proof state after:
no goals
Theorem: Fin.cons.norm
Proof 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
Proof state after:
no goals
Theorem: Fin.cons.map_sub
Proof 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)) → AddGroup (α i)
a c : α 0
b d : (i : Fin n) → α (succ i)
⊢ cons a b - cons c d = cons (a - c) (b - d)
Tactic:
ext i
Proof state after:
case h
𝕜 : 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)) → AddGroup (α i)
a c : α 0
b d : (i : Fin n) → α (succ i)
i : Fin (n + 1)
⊢ (cons a b - cons c d) i = cons (a - c) (b - d) i
Theorem: Fin.cons.map_sub
Proof state before:
case h
𝕜 : 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)) → AddGroup (α i)
a c : α 0
b d : (i : Fin n) → α (succ i)
i : Fin (n + 1)
⊢ (cons a b - cons c d) i = cons (a - c) (b - d) i
Tactic:
cases i using Fin.cases <;> simp
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof 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
⊢ Continuous compContinuousLinearMapL
Tactic:
rw [Metric.continuous_iff
  (β := ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G)]
Proof 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
⊢ ∀ (b : (i : Fin n) → E i →L[𝕜] E₁ i),
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ (a : (i : Fin n) → E i →L[𝕜] E₁ i),
          dist a b < δ → dist (compContinuousLinearMapL a) (compContinuousLinearMapL b) < ε
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof 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
⊢ ∀ (b : (i : Fin n) → E i →L[𝕜] E₁ i),
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ (a : (i : Fin n) → E i →L[𝕜] E₁ i),
          dist a b < δ → dist (compContinuousLinearMapL a) (compContinuousLinearMapL b) < ε
Tactic:
simp only [dist_eq_norm_sub]
Proof 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
⊢ ∀ (b : (i : Fin n) → E i →L[𝕜] E₁ i),
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ (a : (i : Fin n) → E i →L[𝕜] E₁ i),
          ‖a - b‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL b‖ < ε
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof 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
⊢ ∀ (b : (i : Fin n) → E i →L[𝕜] E₁ i),
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ (a : (i : Fin n) → E i →L[𝕜] E₁ i),
          ‖a - b‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL b‖ < ε
Tactic:
intro f
Proof 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
f : (i : Fin n) → E i →L[𝕜] E₁ i
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ (a : (i : Fin n) → E i →L[𝕜] E₁ i), ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case zero
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
E : Fin Nat.zero → Type u_2
inst✝³ : (i : Fin Nat.zero) → NormedAddCommGroup (E i)
inst✝² : (i : Fin Nat.zero) → NormedSpace 𝕜 (E i)
E₁ : Fin Nat.zero → Type u_3
inst✝¹ : (i : Fin Nat.zero) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin Nat.zero) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin Nat.zero) → E i →L[𝕜] E₁ i
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ (a : (i : Fin Nat.zero) → E i →L[𝕜] E₁ i),
        ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
Tactic:
exact fun ε hε ↦ ⟨1, ⟨zero_lt_one, fun g _ ↦ by simp [Subsingleton.elim f g, hε]⟩⟩
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
E : Fin Nat.zero → Type u_2
inst✝³ : (i : Fin Nat.zero) → NormedAddCommGroup (E i)
inst✝² : (i : Fin Nat.zero) → NormedSpace 𝕜 (E i)
E₁ : Fin Nat.zero → Type u_3
inst✝¹ : (i : Fin Nat.zero) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin Nat.zero) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin Nat.zero) → E i →L[𝕜] E₁ i
ε : ℝ
hε : ε > 0
g : (i : Fin Nat.zero) → E i →L[𝕜] E₁ i
x✝ : ‖g - f‖ < 1
⊢ ‖compContinuousLinearMapL g - compContinuousLinearMapL f‖ < ε
Tactic:
simp [Subsingleton.elim f g, hε]
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case succ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
IH :
  ∀ {E : Fin n → Type u_2} [inst : (i : Fin n) → NormedAddCommGroup (E i)] [inst_1 : (i : Fin n) → NormedSpace 𝕜 (E i)]
    {E₁ : Fin n → Type u_3} [inst_2 : (i : Fin n) → NormedAddCommGroup (E₁ i)]
    [inst_3 : (i : Fin n) → NormedSpace 𝕜 (E₁ i)] (f : (i : Fin n) → E i →L[𝕜] E₁ i),
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ (a : (i : Fin n) → E i →L[𝕜] E₁ i),
          ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ (a : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i),
        ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
Tactic:
intro ε hε_pos
Proof state after:
case succ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
IH :
  ∀ {E : Fin n → Type u_2} [inst : (i : Fin n) → NormedAddCommGroup (E i)] [inst_1 : (i : Fin n) → NormedSpace 𝕜 (E i)]
    {E₁ : Fin n → Type u_3} [inst_2 : (i : Fin n) → NormedAddCommGroup (E₁ i)]
    [inst_3 : (i : Fin n) → NormedSpace 𝕜 (E₁ i)] (f : (i : Fin n) → E i →L[𝕜] E₁ i),
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ (a : (i : Fin n) → E i →L[𝕜] E₁ i),
          ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
⊢ ∃ δ > 0,
    ∀ (a : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i),
      ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case succ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
IH :
  ∀ {E : Fin n → Type u_2} [inst : (i : Fin n) → NormedAddCommGroup (E i)] [inst_1 : (i : Fin n) → NormedSpace 𝕜 (E i)]
    {E₁ : Fin n → Type u_3} [inst_2 : (i : Fin n) → NormedAddCommGroup (E₁ i)]
    [inst_3 : (i : Fin n) → NormedSpace 𝕜 (E₁ i)] (f : (i : Fin n) → E i →L[𝕜] E₁ i),
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ (a : (i : Fin n) → E i →L[𝕜] E₁ i),
          ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
⊢ ∃ δ > 0,
    ∀ (a : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i),
      ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
Tactic:
generalize hε₁_def : (ε / 2) / (2 + ‖f 0‖) = ε₁
Proof state after:
case succ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
IH :
  ∀ {E : Fin n → Type u_2} [inst : (i : Fin n) → NormedAddCommGroup (E i)] [inst_1 : (i : Fin n) → NormedSpace 𝕜 (E i)]
    {E₁ : Fin n → Type u_3} [inst_2 : (i : Fin n) → NormedAddCommGroup (E₁ i)]
    [inst_3 : (i : Fin n) → NormedSpace 𝕜 (E₁ i)] (f : (i : Fin n) → E i →L[𝕜] E₁ i),
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ (a : (i : Fin n) → E i →L[𝕜] E₁ i),
          ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
⊢ ∃ δ > 0,
    ∀ (a : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i),
      ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
Theorem: ContinuousMultilinearMap.continuous_compContinuousLinearMapL_fin
Proof state before:
case succ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
IH :
  ∀ {E : Fin n → Type u_2} [inst : (i : Fin n) → NormedAddCommGroup (E i)] [inst_1 : (i : Fin n) → NormedSpace 𝕜 (E i)]
    {E₁ : Fin n → Type u_3} [inst_2 : (i : Fin n) → NormedAddCommGroup (E₁ i)]
    [inst_3 : (i : Fin n) → NormedSpace 𝕜 (E₁ i)] (f : (i : Fin n) → E i →L[𝕜] E₁ i),
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ (a : (i : Fin n) → E i →L[𝕜] E₁ i),
          ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
⊢ ∃ δ > 0,
    ∀ (a : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i),
      ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
Tactic:
have hε₁_pos : 0 < ε₁ := by
  rw [← hε₁_def]
  exact div_pos (half_pos hε_pos) <| add_pos_of_pos_of_nonneg zero_lt_two (norm_nonneg _)
Proof state after:
case succ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
IH :
  ∀ {E : Fin n → Type u_2} [inst : (i : Fin n) → NormedAddCommGroup (E i)] [inst_1 : (i : Fin n) → NormedSpace 𝕜 (E i)]
    {E₁ : Fin n → Type u_3} [inst_2 : (i : Fin n) → NormedAddCommGroup (E₁ i)]
    [inst_3 : (i : Fin n) → NormedSpace 𝕜 (E₁ i)] (f : (i : Fin n) → E i →L[𝕜] E₁ i),
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ (a : (i : Fin n) → E i →L[𝕜] E₁ i),
          ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
hε₁_pos : 0 < ε₁
⊢ ∃ δ > 0,
    ∀ (a : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i),
      ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε