α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
⊢ UniformContinuous Subtype.val
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
⊢ UniformContinuous Subtype.val
have hp : p ≠ 0 := (zero_lt_one.trans_le _i.elim).ne'
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
⊢ ∀ (i : α), UniformContinuous fun x => ↑x i
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
⊢ UniformContinuous Subtype.val
rw [uniformContinuous_pi]
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
⊢ UniformContinuous fun x => ↑x i
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
⊢ ∀ (i : α), UniformContinuous fun x => ↑x i
intro i
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
⊢ ∀ (i_1 : ℝ),
    0 < i_1 →
      ∃ j,
        0 < j ∧
          ∀ (x y : { x // x ∈ lp E p }),
            (x, y) ∈ {p_1 | ‖p_1.fst - p_1.snd‖ < j} → (↑x i, ↑y i) ∈ {p | ‖p.fst - p.snd‖ < i_1}
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
⊢ UniformContinuous fun x => ↑x i
rw [NormedAddCommGroup.uniformity_basis_dist.uniformContinuous_iff
  NormedAddCommGroup.uniformity_basis_dist]
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
ε : ℝ
hε : 0 < ε
⊢ ∃ j,
    0 < j ∧
      ∀ (x y : { x // x ∈ lp E p }), (x, y) ∈ {p_1 | ‖p_1.fst - p_1.snd‖ < j} → (↑x i, ↑y i) ∈ {p | ‖p.fst - p.snd‖ < ε}
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
⊢ ∀ (i_1 : ℝ),
    0 < i_1 →
      ∃ j,
        0 < j ∧
          ∀ (x y : { x // x ∈ lp E p }),
            (x, y) ∈ {p_1 | ‖p_1.fst - p_1.snd‖ < j} → (↑x i, ↑y i) ∈ {p | ‖p.fst - p.snd‖ < i_1}
intro ε hε
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
ε : ℝ
hε : 0 < ε
⊢ ∀ (x y : { x // x ∈ lp E p }), (x, y) ∈ {p_1 | ‖p_1.fst - p_1.snd‖ < ε} → (↑x i, ↑y i) ∈ {p | ‖p.fst - p.snd‖ < ε}
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
ε : ℝ
hε : 0 < ε
⊢ ∃ j,
    0 < j ∧
      ∀ (x y : { x // x ∈ lp E p }), (x, y) ∈ {p_1 | ‖p_1.fst - p_1.snd‖ < j} → (↑x i, ↑y i) ∈ {p | ‖p.fst - p.snd‖ < ε}
refine' ⟨ε, hε, _⟩
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
ε : ℝ
hε : 0 < ε
f g : { x // x ∈ lp E p }
hfg : ‖f - g‖ < ε
⊢ (↑f i, ↑g i) ∈ {p | ‖p.fst - p.snd‖ < ε}
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
ε : ℝ
hε : 0 < ε
⊢ ∀ (x y : { x // x ∈ lp E p }), (x, y) ∈ {p_1 | ‖p_1.fst - p_1.snd‖ < ε} → (↑x i, ↑y i) ∈ {p | ‖p.fst - p.snd‖ < ε}
rintro f g (hfg : ‖f - g‖ < ε)
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
ε : ℝ
hε : 0 < ε
f g : { x // x ∈ lp E p }
hfg : ‖f - g‖ < ε
this : ‖↑f i - ↑g i‖ ≤ ‖f - g‖
⊢ (↑f i, ↑g i) ∈ {p | ‖p.fst - p.snd‖ < ε}
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
ε : ℝ
hε : 0 < ε
f g : { x // x ∈ lp E p }
hfg : ‖f - g‖ < ε
⊢ (↑f i, ↑g i) ∈ {p | ‖p.fst - p.snd‖ < ε}
have : ‖f i - g i‖ ≤ ‖f - g‖ := norm_apply_le_norm hp (f - g) i
no goals
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
hp : p ≠ 0
i : α
ε : ℝ
hε : 0 < ε
f g : { x // x ∈ lp E p }
hfg : ‖f - g‖ < ε
this : ‖↑f i - ↑g i‖ ≤ ‖f - g‖
⊢ (↑f i, ↑g i) ∈ {p | ‖p.fst - p.snd‖ < ε}
exact this.trans_lt hfg