internlm/Lean-Github huggingface dataset:
Theorem: ContinuousMultilinearMap.continuous_constOfIsEmpty
Proof 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
⊢ ∀ (b : G), ∀ ε > 0, ∃ δ > 0, ∀ (a : G), dist a b < δ → dist (constOfIsEmpty 𝕜 E a) (constOfIsEmpty 𝕜 E b) < ε
Tactic:
intro y ε hε
Proof state after:
ι : 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
y : G
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0, ∀ (a : G), dist a y < δ → dist (constOfIsEmpty 𝕜 E a) (constOfIsEmpty 𝕜 E y) < ε
Theorem: ContinuousMultilinearMap.continuous_constOfIsEmpty
Proof 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
y : G
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0, ∀ (a : G), dist a y < δ → dist (constOfIsEmpty 𝕜 E a) (constOfIsEmpty 𝕜 E y) < ε
Tactic:
use ε
Proof 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
y : G
ε : ℝ
hε : ε > 0
⊢ ε > 0 ∧ ∀ (a : G), dist a y < ε → dist (constOfIsEmpty 𝕜 E a) (constOfIsEmpty 𝕜 E y) < ε
Theorem: ContinuousMultilinearMap.continuous_constOfIsEmpty
Proof 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
y : G
ε : ℝ
hε : ε > 0
⊢ ε > 0 ∧ ∀ (a : G), dist a y < ε → dist (constOfIsEmpty 𝕜 E a) (constOfIsEmpty 𝕜 E y) < ε
Tactic:
refine And.intro hε ?_
Proof 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
y : G
ε : ℝ
hε : ε > 0
⊢ ∀ (a : G), dist a y < ε → dist (constOfIsEmpty 𝕜 E a) (constOfIsEmpty 𝕜 E y) < ε
Theorem: ContinuousMultilinearMap.continuous_constOfIsEmpty
Proof 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
y : G
ε : ℝ
hε : ε > 0
⊢ ∀ (a : G), dist a y < ε → dist (constOfIsEmpty 𝕜 E a) (constOfIsEmpty 𝕜 E y) < ε
Tactic:
intro x h
Proof 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
y : G
ε : ℝ
hε : ε > 0
x : G
h : dist x y < ε
⊢ dist (constOfIsEmpty 𝕜 E x) (constOfIsEmpty 𝕜 E y) < ε
Theorem: ContinuousMultilinearMap.continuous_constOfIsEmpty
Proof 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
y : G
ε : ℝ
hε : ε > 0
x : G
h : dist x y < ε
⊢ dist (constOfIsEmpty 𝕜 E x) (constOfIsEmpty 𝕜 E y) < ε
Tactic:
rw [dist_eq_norm] at h ⊢
Proof 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
y : G
ε : ℝ
hε : ε > 0
x : G
h : ‖x - y‖ < ε
⊢ ‖constOfIsEmpty 𝕜 E x - constOfIsEmpty 𝕜 E y‖ < ε
Theorem: ContinuousMultilinearMap.continuous_constOfIsEmpty
Proof 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
y : G
ε : ℝ
hε : ε > 0
x : G
h : ‖x - y‖ < ε
⊢ ‖constOfIsEmpty 𝕜 E x - constOfIsEmpty 𝕜 E y‖ < ε
Tactic:
change ‖constOfIsEmpty 𝕜 E (x - y)‖ < ε
Proof 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
y : G
ε : ℝ
hε : ε > 0
x : G
h : ‖x - y‖ < ε
⊢ ‖constOfIsEmpty 𝕜 E (x - y)‖ < ε
Theorem: ContinuousMultilinearMap.continuous_constOfIsEmpty
Proof 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
y : G
ε : ℝ
hε : ε > 0
x : G
h : ‖x - y‖ < ε
⊢ ‖constOfIsEmpty 𝕜 E (x - y)‖ < ε
Tactic:
rw [norm_constOfIsEmpty]
Proof 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
y : G
ε : ℝ
hε : ε > 0
x : G
h : ‖x - y‖ < ε
⊢ ‖x - y‖ < ε
Theorem: ContinuousMultilinearMap.continuous_constOfIsEmpty
Proof 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
y : G
ε : ℝ
hε : ε > 0
x : G
h : ‖x - y‖ < ε
⊢ ‖x - y‖ < ε
Tactic:
exact h
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.domDomCongrLinearEquiv'_apply_piCongrLeft'
Proof state before:
R : Type u_1
inst✝¹⁰ : Semiring R
S : Type u_2
inst✝⁹ : Semiring S
ι : Type u_3
inst✝⁸ : Fintype ι
ι' : Type u_4
inst✝⁷ : Fintype ι'
D : ι → Type u_5
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝⁵ : (i : ι) → Module R (D i)
F : Type u_6
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module R F
inst✝² : Module S F
inst✝¹ : ContinuousConstSMul S F
inst✝ : SMulCommClass R S F
σ : ι ≃ ι'
f : ContinuousMultilinearMap R D F
x : (i : ι) → D i
⊢ ((domDomCongrLinearEquiv' R S D F σ) f) ((Equiv.piCongrLeft' D σ) x) = f x
Tactic:
rw [domDomCongrLinearEquiv'_apply, Equiv.symm_apply_apply]
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.domDomCongrLinearEquiv'_symm_apply_piCongrLeft'_symm
Proof state before:
R : Type u_1
inst✝¹⁰ : Semiring R
S : Type u_2
inst✝⁹ : Semiring S
ι : Type u_3
inst✝⁸ : Fintype ι
ι' : Type u_4
inst✝⁷ : Fintype ι'
D : ι → Type u_5
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝⁵ : (i : ι) → Module R (D i)
F : Type u_6
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module R F
inst✝² : Module S F
inst✝¹ : ContinuousConstSMul S F
inst✝ : SMulCommClass R S F
σ : ι ≃ ι'
f : ContinuousMultilinearMap R (fun i => D (σ.symm i)) F
x : (i' : ι') → D (σ.symm i')
⊢ ((LinearEquiv.symm (domDomCongrLinearEquiv' R S D F σ)) f) ((Equiv.piCongrLeft' D σ).symm x) = f x
Tactic:
rw [domDomCongrLinearEquiv'_symm_apply, Equiv.apply_symm_apply]
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.norm_domDomCongrLinearEquiv'
Proof state before:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
⊢ ‖(domDomCongrLinearEquiv' 𝕜 𝕜 D F σ) f‖ = ‖f‖
Tactic:
simp only [ContinuousMultilinearMap.norm_def, domDomCongrLinearEquiv'_apply]
Proof state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
⊢ sInf {c | 0 ≤ c ∧ ∀ (m : (i : ι') → D (σ.symm i)), ‖f ((Equiv.piCongrLeft' D σ).symm m)‖ ≤ c * ∏ i : ι', ‖m i‖} =
    sInf {c | 0 ≤ c ∧ ∀ (m : (i : ι) → D i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}
Theorem: ContinuousMultilinearMap.norm_domDomCongrLinearEquiv'
Proof state before:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
⊢ sInf {c | 0 ≤ c ∧ ∀ (m : (i : ι') → D (σ.symm i)), ‖f ((Equiv.piCongrLeft' D σ).symm m)‖ ≤ c * ∏ i : ι', ‖m i‖} =
    sInf {c | 0 ≤ c ∧ ∀ (m : (i : ι) → D i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}
Tactic:
refine congrArg _ ?_
Proof state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
⊢ {c | 0 ≤ c ∧ ∀ (m : (i : ι') → D (σ.symm i)), ‖f ((Equiv.piCongrLeft' D σ).symm m)‖ ≤ c * ∏ i : ι', ‖m i‖} =
    {c | 0 ≤ c ∧ ∀ (m : (i : ι) → D i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}
Theorem: ContinuousMultilinearMap.norm_domDomCongrLinearEquiv'
Proof state before:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
⊢ {c | 0 ≤ c ∧ ∀ (m : (i : ι') → D (σ.symm i)), ‖f ((Equiv.piCongrLeft' D σ).symm m)‖ ≤ c * ∏ i : ι', ‖m i‖} =
    {c | 0 ≤ c ∧ ∀ (m : (i : ι) → D i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}
Tactic:
ext c
Proof state after:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
⊢ c ∈ {c | 0 ≤ c ∧ ∀ (m : (i : ι') → D (σ.symm i)), ‖f ((Equiv.piCongrLeft' D σ).symm m)‖ ≤ c * ∏ i : ι', ‖m i‖} ↔
    c ∈ {c | 0 ≤ c ∧ ∀ (m : (i : ι) → D i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}
Theorem: ContinuousMultilinearMap.norm_domDomCongrLinearEquiv'
Proof state before:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
⊢ c ∈ {c | 0 ≤ c ∧ ∀ (m : (i : ι') → D (σ.symm i)), ‖f ((Equiv.piCongrLeft' D σ).symm m)‖ ≤ c * ∏ i : ι', ‖m i‖} ↔
    c ∈ {c | 0 ≤ c ∧ ∀ (m : (i : ι) → D i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}
Tactic:
simp only [Set.mem_setOf_eq, and_congr_right_iff]
Proof state after:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
⊢ 0 ≤ c →
    ((∀ (m : (i : ι') → D (σ.symm i)), ‖f ((Equiv.piCongrLeft' D σ).symm m)‖ ≤ c * ∏ i : ι', ‖m i‖) ↔
      ∀ (m : (i : ι) → D i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖)
Theorem: ContinuousMultilinearMap.norm_domDomCongrLinearEquiv'
Proof state before:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
⊢ 0 ≤ c →
    ((∀ (m : (i : ι') → D (σ.symm i)), ‖f ((Equiv.piCongrLeft' D σ).symm m)‖ ≤ c * ∏ i : ι', ‖m i‖) ↔
      ∀ (m : (i : ι) → D i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖)
Tactic:
intro _
Proof state after:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
a✝ : 0 ≤ c
⊢ (∀ (m : (i : ι') → D (σ.symm i)), ‖f ((Equiv.piCongrLeft' D σ).symm m)‖ ≤ c * ∏ i : ι', ‖m i‖) ↔
    ∀ (m : (i : ι) → D i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖
Theorem: ContinuousMultilinearMap.norm_domDomCongrLinearEquiv'
Proof state before:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
a✝ : 0 ≤ c
⊢ (∀ (m : (i : ι') → D (σ.symm i)), ‖f ((Equiv.piCongrLeft' D σ).symm m)‖ ≤ c * ∏ i : ι', ‖m i‖) ↔
    ∀ (m : (i : ι) → D i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖
Tactic:
rw [Equiv.forall_congr_left' (Equiv.piCongrLeft' D σ).symm]
Proof state after:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
a✝ : 0 ≤ c
⊢ (∀ (y : (a : ι) → D a),
      ‖f ((Equiv.piCongrLeft' D σ).symm ((Equiv.piCongrLeft' D σ).symm.symm y))‖ ≤
        c * ∏ i : ι', ‖(Equiv.piCongrLeft' D σ).symm.symm y i‖) ↔
    ∀ (m : (i : ι) → D i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖
Theorem: ContinuousMultilinearMap.norm_domDomCongrLinearEquiv'
Proof state before:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
a✝ : 0 ≤ c
⊢ (∀ (y : (a : ι) → D a),
      ‖f ((Equiv.piCongrLeft' D σ).symm ((Equiv.piCongrLeft' D σ).symm.symm y))‖ ≤
        c * ∏ i : ι', ‖(Equiv.piCongrLeft' D σ).symm.symm y i‖) ↔
    ∀ (m : (i : ι) → D i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖
Tactic:
simp only [Equiv.symm_symm, Equiv.symm_apply_apply, Equiv.piCongrLeft'_apply]
Proof state after:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
a✝ : 0 ≤ c
⊢ (∀ (y : (a : ι) → D a), ‖f y‖ ≤ c * ∏ x : ι', ‖y (σ.symm x)‖) ↔ ∀ (m : (i : ι) → D i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖
Theorem: ContinuousMultilinearMap.norm_domDomCongrLinearEquiv'
Proof state before:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
a✝ : 0 ≤ c
⊢ (∀ (y : (a : ι) → D a), ‖f y‖ ≤ c * ∏ x : ι', ‖y (σ.symm x)‖) ↔ ∀ (m : (i : ι) → D i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖
Tactic:
rw [forall_congr]
Proof state after:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
a✝ : 0 ≤ c
⊢ ∀ (a : (a : ι) → D a), (‖f a‖ ≤ c * ∏ x : ι', ‖a (σ.symm x)‖) = (‖f a‖ ≤ c * ∏ i : ι, ‖a i‖)
Theorem: ContinuousMultilinearMap.norm_domDomCongrLinearEquiv'
Proof state before:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
a✝ : 0 ≤ c
⊢ ∀ (a : (a : ι) → D a), (‖f a‖ ≤ c * ∏ x : ι', ‖a (σ.symm x)‖) = (‖f a‖ ≤ c * ∏ i : ι, ‖a i‖)
Tactic:
intro x
Proof state after:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
a✝ : 0 ≤ c
x : (a : ι) → D a
⊢ (‖f x‖ ≤ c * ∏ x_1 : ι', ‖x (σ.symm x_1)‖) = (‖f x‖ ≤ c * ∏ i : ι, ‖x i‖)
Theorem: ContinuousMultilinearMap.norm_domDomCongrLinearEquiv'
Proof state before:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
a✝ : 0 ≤ c
x : (a : ι) → D a
⊢ (‖f x‖ ≤ c * ∏ x_1 : ι', ‖x (σ.symm x_1)‖) = (‖f x‖ ≤ c * ∏ i : ι, ‖x i‖)
Tactic:
rw [eq_iff_iff]
Proof state after:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
a✝ : 0 ≤ c
x : (a : ι) → D a
⊢ ‖f x‖ ≤ c * ∏ x_1 : ι', ‖x (σ.symm x_1)‖ ↔ ‖f x‖ ≤ c * ∏ i : ι, ‖x i‖
Theorem: ContinuousMultilinearMap.norm_domDomCongrLinearEquiv'
Proof state before:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
a✝ : 0 ≤ c
x : (a : ι) → D a
⊢ ‖f x‖ ≤ c * ∏ x_1 : ι', ‖x (σ.symm x_1)‖ ↔ ‖f x‖ ≤ c * ∏ i : ι, ‖x i‖
Tactic:
rw [← Finset.univ_map_equiv_to_embedding σ, Finset.prod_map]
Proof state after:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
a✝ : 0 ≤ c
x : (a : ι) → D a
⊢ ‖f x‖ ≤ c * ∏ x_1 : ι, ‖x (σ.symm ((Equiv.toEmbedding σ) x_1))‖ ↔ ‖f x‖ ≤ c * ∏ i : ι, ‖x i‖
Theorem: ContinuousMultilinearMap.norm_domDomCongrLinearEquiv'
Proof state before:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
a✝ : 0 ≤ c
x : (a : ι) → D a
⊢ ‖f x‖ ≤ c * ∏ x_1 : ι, ‖x (σ.symm ((Equiv.toEmbedding σ) x_1))‖ ↔ ‖f x‖ ≤ c * ∏ i : ι, ‖x i‖
Tactic:
simp only [Equiv.coe_toEmbedding]
Proof state after:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝⁵ : Fintype ι
ι' : Type u_3
inst✝⁴ : Fintype ι'
D : ι → Type u_4
inst✝³ : (i : ι) → SeminormedAddCommGroup (D i)
inst✝² : (i : ι) → NormedSpace 𝕜 (D i)
F : Type u_5
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
σ : ι ≃ ι'
f : ContinuousMultilinearMap 𝕜 D F
c : ℝ
a✝ : 0 ≤ c
x : (a : ι) → D a
⊢ ‖f x‖ ≤ c * ∏ x_1 : ι, ‖x (σ.symm (σ x_1))‖ ↔ ‖f x‖ ≤ c * ∏ i : ι, ‖x i‖
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
α : Type u_5
δ₁ : Type u_6
n : ℕ
f : Fin (Nat.succ n) → α → δ₁
x : α
p : Fin n → α
⊢ (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
α : 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