Theorem: diam_closedBall_eq (Ray/Hartogs/Hartogs.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
⊢ Metric.diam (closedBall c r) = 2 * r
Tactic:
apply le_antisymm (Metric.diam_closedBall rp)
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
⊢ 2 * r ≤ Metric.diam (closedBall c r)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
⊢ 2 * r ≤ Metric.diam (closedBall c r)
Tactic:
trans Metric.diam (ball c r)
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
⊢ 2 * r ≤ Metric.diam (ball c r)

E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
⊢ Metric.diam (ball c r) ≤ Metric.diam (closedBall c r)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
⊢ 2 * r ≤ Metric.diam (ball c r)

E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
⊢ Metric.diam (ball c r) ≤ Metric.diam (closedBall c r)
Tactic:
rw [diam_ball_eq rp]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
⊢ Metric.diam (ball c r) ≤ Metric.diam (closedBall c r)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c0' c1 z0 z1 w0 w1 : ℂ
r✝ r0 r1 b e : ℝ
c : ℂ
r : ℝ
rp : r ≥ 0
⊢ Metric.diam (ball c r) ≤ Metric.diam (closedBall c r)
Tactic:
exact Metric.diam_mono Metric.ball_subset_closedBall Metric.isBounded_closedBall
State after:
no goals