α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
⊢ dist (embeddingOfSubset x a) (embeddingOfSubset x b) = dist a b
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a b : α
H : DenseRange x
⊢ Isometry (embeddingOfSubset x)
refine' Isometry.of_dist_eq fun a b => _
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
⊢ dist (embeddingOfSubset x a) (embeddingOfSubset x b) = dist a b
refine' (embeddingOfSubset_dist_le x a b).antisymm (le_of_forall_pos_le_add fun e epos => _)
case intro
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
rcases Metric.mem_closure_range_iff.1 (H a) (e / 2) (half_pos epos) with ⟨n, hn⟩
case intro
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
case intro
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
have C : dist b (x n) - dist a (x n) = embeddingOfSubset x b n - embeddingOfSubset x a n := by
  simp only [embeddingOfSubset_coe, sub_sub_sub_cancel_right]
case intro
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
this : dist a b ≤ dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
case intro
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
have :=
  calc
    dist a b ≤ dist a (x n) + dist (x n) b := dist_triangle _ _ _
    _ = 2 * dist a (x n) + (dist b (x n) - dist a (x n)) := by simp [dist_comm]; ring
    _ ≤ 2 * dist a (x n) + |dist b (x n) - dist a (x n)| := by
      apply_rules [add_le_add_left, le_abs_self]
    _ ≤ 2 * (e / 2) + |embeddingOfSubset x b n - embeddingOfSubset x a n| := by
      rw [C]
      apply_rules [add_le_add, mul_le_mul_of_nonneg_left, hn.le, le_refl]
      norm_num
    _ ≤ 2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a) := by
      have : |embeddingOfSubset x b n - embeddingOfSubset x a n| ≤
          dist (embeddingOfSubset x b) (embeddingOfSubset x a) := by
        simp only [dist_eq_norm]
        exact lp.norm_apply_le_norm ENNReal.top_ne_zero
          (embeddingOfSubset x b - embeddingOfSubset x a) n
      nlinarith
    _ = dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e := by ring
no goals
case intro
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
this : dist a b ≤ dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
simpa [dist_comm] using this
no goals
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
⊢ dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
simp only [embeddingOfSubset_coe, sub_sub_sub_cancel_right]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ dist a (x n) + dist b (x n) = 2 * dist a (x n) + (dist b (x n) - dist a (x n))
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ dist a (x n) + dist (x n) b = 2 * dist a (x n) + (dist b (x n) - dist a (x n))
simp [dist_comm]
no goals
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ dist a (x n) + dist b (x n) = 2 * dist a (x n) + (dist b (x n) - dist a (x n))
ring
no goals
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ 2 * dist a (x n) + (dist b (x n) - dist a (x n)) ≤ 2 * dist a (x n) + abs (dist b (x n) - dist a (x n))
apply_rules [add_le_add_left, le_abs_self]
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ 2 * dist a (x n) + abs (↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n) ≤
    2 * (e / 2) + abs (↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n)
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ 2 * dist a (x n) + abs (dist b (x n) - dist a (x n)) ≤
    2 * (e / 2) + abs (↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n)
rw [C]
case h₁.a0
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
C_symm : ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n = dist b (x n) - dist a (x n)
⊢ 0 ≤ 2
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ 2 * dist a (x n) + abs (↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n) ≤
    2 * (e / 2) + abs (↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n)
apply_rules [add_le_add, mul_le_mul_of_nonneg_left, hn.le, le_refl]
no goals
case h₁.a0
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
C_symm : ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n = dist b (x n) - dist a (x n)
⊢ 0 ≤ 2
norm_num
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
this :
  abs (↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n) ≤ dist (embeddingOfSubset x b) (embeddingOfSubset x a)
⊢ 2 * (e / 2) + abs (↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n) ≤
    2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a)
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ 2 * (e / 2) + abs (↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n) ≤
    2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a)
have : |embeddingOfSubset x b n - embeddingOfSubset x a n| ≤
    dist (embeddingOfSubset x b) (embeddingOfSubset x a) := by
  simp only [dist_eq_norm]
  exact lp.norm_apply_le_norm ENNReal.top_ne_zero
    (embeddingOfSubset x b - embeddingOfSubset x a) n
no goals
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
this :
  abs (↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n) ≤ dist (embeddingOfSubset x b) (embeddingOfSubset x a)
⊢ 2 * (e / 2) + abs (↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n) ≤
    2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a)
nlinarith
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ abs (↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n) ≤ ‖embeddingOfSubset x b - embeddingOfSubset x a‖
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ abs (↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n) ≤ dist (embeddingOfSubset x b) (embeddingOfSubset x a)
simp only [dist_eq_norm]
no goals
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ abs (↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n) ≤ ‖embeddingOfSubset x b - embeddingOfSubset x a‖
exact lp.norm_apply_le_norm ENNReal.top_ne_zero
  (embeddingOfSubset x b - embeddingOfSubset x a) n
no goals
α : Type u
β : Type v
γ : Type w
f g : { x // x ∈ lp (fun n => ℝ) ⊤ }
n✝ : ℕ
C✝ : ℝ
inst✝ : MetricSpace α
x : ℕ → α
a✝ b✝ : α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ 2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a) =
    dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e
ring