α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ a b : α
n : ℕ
⊢ ‖↑(embeddingOfSubset x a - embeddingOfSubset x b) n‖ ≤ dist a b
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ a b : α
⊢ dist (embeddingOfSubset x a) (embeddingOfSubset x b) ≤ dist a b
refine' lp.norm_le_of_forall_le dist_nonneg fun n => _
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ a b : α
n : ℕ
⊢ ‖dist a (x n) - dist (x 0) (x n) - (dist b (x n) - dist (x 0) (x n))‖ ≤ dist a b
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ a b : α
n : ℕ
⊢ ‖↑(embeddingOfSubset x a - embeddingOfSubset x b) n‖ ≤ dist a b
simp only [lp.coeFn_sub, Pi.sub_apply, embeddingOfSubset_coe, Real.dist_eq]
case h.e'_3.h.e'_1
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ a b : α
n : ℕ
⊢ dist a (x n) - dist (x 0) (x n) - (dist b (x n) - dist (x 0) (x n)) = dist a (x n) - dist b (x n)
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ a b : α
n : ℕ
⊢ ‖dist a (x n) - dist (x 0) (x n) - (dist b (x n) - dist (x 0) (x n))‖ ≤ dist a b
convert abs_dist_sub_le a b (x n) using 2
no goals
case h.e'_3.h.e'_1
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ a b : α
n : ℕ
⊢ dist a (x n) - dist (x 0) (x n) - (dist b (x n) - dist (x 0) (x n)) = dist a (x n) - dist b (x n)
ring