lean_workbook_plus_71420
ProvedProve that U is a linear subspace U=\left \\{ f\\in \\mathbb{R}^{\\mathbb{R}} \\mid f(x)=f(-x),\\forall \\in \\mathbb{R}\\right \\} is a linear subspace in .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_71420 (U : Set (ℝ → ℝ)) (hU : U = {f : ℝ → ℝ | ∀ x, f x = f (-x)}) : (∀ f g : ℝ → ℝ, f ∈ U ∧ g ∈ U → f + g ∈ U) ∧ (∀ f : ℝ → ℝ, f ∈ U → ∀ c : ℝ, c • f ∈ U) := by sorrySource