case h
F : Type ?u.1619749
α : Type u
β : Type v
γ : Type w
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ ↑f x = (toReal ∘ ↑(nnrealPart f) - toReal ∘ ↑(nnrealPart (-f))) x
F : Type ?u.1619749
α : Type u
β : Type v
γ : Type w
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
⊢ ↑f = toReal ∘ ↑(nnrealPart f) - toReal ∘ ↑(nnrealPart (-f))
funext x
case h
F : Type ?u.1619749
α : Type u
β : Type v
γ : Type w
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ ↑f x = max (↑f x) 0 - max (-↑f x) 0
case h
F : Type ?u.1619749
α : Type u
β : Type v
γ : Type w
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ ↑f x = (toReal ∘ ↑(nnrealPart f) - toReal ∘ ↑(nnrealPart (-f))) x
dsimp
no goals
case h
F : Type ?u.1619749
α : Type u
β : Type v
γ : Type w
inst✝ : TopologicalSpace α
f : α →ᵇ ℝ
x : α
⊢ ↑f x = max (↑f x) 0 - max (-↑f x) 0
simp only [max_zero_sub_max_neg_zero_eq_self]