x y : ℝ
⊢ Continuous fun x => log ↑x
x y : ℝ
⊢ ContinuousOn log ({0}ᶜ)
simp only [continuousOn_iff_continuous_restrict, restrict]
x y : ℝ
⊢ Continuous fun x => ↑(OrderIso.symm expOrderIso) { val := abs ↑x, property := (_ : 0 < abs ↑x) }
x y : ℝ
⊢ Continuous fun x => log ↑x
conv in log _ => rw [log_of_ne_zero (show (x : ℝ) ≠ 0 from x.2)]
no goals
x y : ℝ
⊢ Continuous fun x => ↑(OrderIso.symm expOrderIso) { val := abs ↑x, property := (_ : 0 < abs ↑x) }
exact expOrderIso.symm.continuous.comp (continuous_subtype_val.norm.subtype_mk _)