ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ (x : ℝ≥0), x ≤ 1 → x ^ p ≤ x
⊢ a ^ p + b ^ p ≤ 1
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ 1
have h_le_one : ∀ x : ℝ≥0, x ≤ 1 → x ^ p ≤ x := fun x hx => rpow_le_self_of_le_one hx hp1
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ (x : ℝ≥0), x ≤ 1 → x ^ p ≤ x
ha : a ≤ 1
⊢ a ^ p + b ^ p ≤ 1
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ (x : ℝ≥0), x ≤ 1 → x ^ p ≤ x
⊢ a ^ p + b ^ p ≤ 1
have ha : a ≤ 1 := (self_le_add_right a b).trans hab
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ (x : ℝ≥0), x ≤ 1 → x ^ p ≤ x
ha : a ≤ 1
hb : b ≤ 1
⊢ a ^ p + b ^ p ≤ 1
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ (x : ℝ≥0), x ≤ 1 → x ^ p ≤ x
ha : a ≤ 1
⊢ a ^ p + b ^ p ≤ 1
have hb : b ≤ 1 := (self_le_add_left b a).trans hab
no goals
ι : Type u
s : Finset ι
p : ℝ
a b : ℝ≥0
hab : a + b ≤ 1
hp1 : 1 ≤ p
h_le_one : ∀ (x : ℝ≥0), x ≤ 1 → x ^ p ≤ x
ha : a ≤ 1
hb : b ≤ 1
⊢ a ^ p + b ^ p ≤ 1
exact (add_le_add (h_le_one a ha) (h_le_one b hb)).trans hab