no goals
s r : ℝ
hs : s < 0
x : ℝ
hx : x ∈ Set.Icc 0 1
⊢ x ∈ {x | (fun x => ((fun x => log x ^ r) ∘ fun x => x⁻¹) x = (fun x => abs (log x) ^ r) x) x}
simp [abs_of_nonpos, log_nonpos hx.1 hx.2]
no goals
s r : ℝ
hs : s < 0
x : ℝ
hx : x ∈ Set.Ioi 0
⊢ ((fun x => x ^ (-s)) ∘ fun x => x⁻¹) x = (fun x => x ^ s) x
rw [Function.comp_apply, inv_rpow hx.out.le, rpow_neg hx.out.le, inv_inv]