case h_one
ι : Type u_2
α : Type u_1
inst✝ : OrderedAddCommGroup α
s✝ t : Interval α
a : α
f : ι → Interval α
s : Finset ι
⊢ length 0 = 0

case h_mul
ι : Type u_2
α : Type u_1
inst✝ : OrderedAddCommGroup α
s✝ t : Interval α
a : α
f : ι → Interval α
s : Finset ι
⊢ ∀ (x y : Interval α), length (x + y) ≤ length x + length y
ι : Type u_2
α : Type u_1
inst✝ : OrderedAddCommGroup α
s✝ t : Interval α
a : α
f : ι → Interval α
s : Finset ι
⊢ length (∑ i in s, f i) ≤ ∑ i in s, length (f i)
apply Finset.le_sum_of_subadditive
case h_mul
ι : Type u_2
α : Type u_1
inst✝ : OrderedAddCommGroup α
s✝ t : Interval α
a : α
f : ι → Interval α
s : Finset ι
⊢ ∀ (x y : Interval α), length (x + y) ≤ length x + length y
case h_one
ι : Type u_2
α : Type u_1
inst✝ : OrderedAddCommGroup α
s✝ t : Interval α
a : α
f : ι → Interval α
s : Finset ι
⊢ length 0 = 0

case h_mul
ι : Type u_2
α : Type u_1
inst✝ : OrderedAddCommGroup α
s✝ t : Interval α
a : α
f : ι → Interval α
s : Finset ι
⊢ ∀ (x y : Interval α), length (x + y) ≤ length x + length y
exact length_zero
no goals
case h_mul
ι : Type u_2
α : Type u_1
inst✝ : OrderedAddCommGroup α
s✝ t : Interval α
a : α
f : ι → Interval α
s : Finset ι
⊢ ∀ (x y : Interval α), length (x + y) ≤ length x + length y
exact length_add_le