Theorem: ContinuousMultilinearMap.continuous_constOfIsEmpty (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
⊢ Continuous fun y => constOfIsEmpty 𝕜 E y
Tactic:
rw [Metric.continuous_iff]
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
⊢ ∀ (b : G), ∀ ε > 0, ∃ δ > 0, ∀ (a : G), dist a b < δ → dist (constOfIsEmpty 𝕜 E a) (constOfIsEmpty 𝕜 E b) < ε

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ε
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) < ε

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 ε
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) < ε

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ε ?_
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) < ε

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
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) < ε

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 ⊢
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‖ < ε

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)‖ < ε
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)‖ < ε

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]
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‖ < ε

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
State after:
no goals