case intro
E : Type u_3
ι : Type u_1
K : Type u_2
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
⊢ Metric.Bounded (fundamentalDomain b)
E : Type u_3
ι : Type u_1
K : Type u_2
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
⊢ Metric.Bounded (fundamentalDomain b)
cases nonempty_fintype ι
case intro
E : Type u_3
ι : Type u_1
K : Type u_2
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
⊢ ∀ (x : E), x ∈ fundamentalDomain b → ∀ (y : E), y ∈ fundamentalDomain b → dist x y ≤ 2 * ∑ j : ι, ‖↑b j‖
case intro
E : Type u_3
ι : Type u_1
K : Type u_2
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
⊢ Metric.Bounded (fundamentalDomain b)
use 2 * ∑ j, ‖b j‖
case intro
E : Type u_3
ι : Type u_1
K : Type u_2
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
y : E
hy : y ∈ fundamentalDomain b
⊢ dist x y ≤ 2 * ∑ j : ι, ‖↑b j‖
case intro
E : Type u_3
ι : Type u_1
K : Type u_2
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
⊢ ∀ (x : E), x ∈ fundamentalDomain b → ∀ (y : E), y ∈ fundamentalDomain b → dist x y ≤ 2 * ∑ j : ι, ‖↑b j‖
intro x hx y hy
case intro
E : Type u_3
ι : Type u_1
K : Type u_2
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
y : E
hy : y ∈ fundamentalDomain b
⊢ ‖x‖ + ‖y‖ ≤ 2 * ∑ j : ι, ‖↑b j‖
case intro
E : Type u_3
ι : Type u_1
K : Type u_2
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
y : E
hy : y ∈ fundamentalDomain b
⊢ dist x y ≤ 2 * ∑ j : ι, ‖↑b j‖
refine le_trans (dist_le_norm_add_norm x y) ?_
case intro
E : Type u_3
ι : Type u_1
K : Type u_2
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
y : E
hy : y ∈ fundamentalDomain b
⊢ ‖fract b x‖ + ‖fract b y‖ ≤ 2 * ∑ j : ι, ‖↑b j‖
case intro
E : Type u_3
ι : Type u_1
K : Type u_2
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
y : E
hy : y ∈ fundamentalDomain b
⊢ ‖x‖ + ‖y‖ ≤ 2 * ∑ j : ι, ‖↑b j‖
rw [← fract_eq_self.mpr hx, ← fract_eq_self.mpr hy]
case intro
E : Type u_3
ι : Type u_1
K : Type u_2
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
y : E
hy : y ∈ fundamentalDomain b
⊢ ∑ i : ι, ‖↑b i‖ + ∑ i : ι, ‖↑b i‖ ≤ 2 * ∑ j : ι, ‖↑b j‖
case intro
E : Type u_3
ι : Type u_1
K : Type u_2
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
y : E
hy : y ∈ fundamentalDomain b
⊢ ‖fract b x‖ + ‖fract b y‖ ≤ 2 * ∑ j : ι, ‖↑b j‖
refine (add_le_add (norm_fract_le b x) (norm_fract_le b y)).trans ?_
no goals
case intro
E : Type u_3
ι : Type u_1
K : Type u_2
inst✝⁵ : NormedLinearOrderedField K
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
b : Basis ι K E
inst✝² : FloorRing K
inst✝¹ : Finite ι
inst✝ : HasSolidNorm K
val✝ : Fintype ι
x : E
hx : x ∈ fundamentalDomain b
y : E
hy : y ∈ fundamentalDomain b
⊢ ∑ i : ι, ‖↑b i‖ + ∑ i : ι, ‖↑b i‖ ≤ 2 * ∑ j : ι, ‖↑b j‖
rw [← two_mul]