please help me

Stream: new members

[Zihao Zhang]

example (ef : FnEven f) (og : FnOdd g) : FnEven fun x ↦ f (g x) := by

intro x

--dsimp

calc

(fun x => f (g x)) x=f (g x):=rfl

_=f (-g x):=by rw [ef]

rw [og,neg_neg]

example (ef : FnEven f) (og : FnOdd g) : FnEven fun x ↦ f (g x) := by

intro x

dsimp

calc

_=f (-g x):=by rw [ef]

rw [og,neg_neg]
why the first is right and the second is wrong?

[Martin Dvořák]

#backticks
#mwe

[Derek Rhodes]

Hi @Zihao Zhang , I'm not sure if this helps, I guessed for the definitions of FnEven or FnOdd, and thought they might be something like this:

import Mathlib.Data.Real.Basic

def FnEven (f: ℝ → ℝ) := ∀ x, f x = f (-x)
def FnOdd (f: ℝ → ℝ) := ∀ x, f (-x) = - f x

example (ef : FnEven f) (og : FnOdd g) : FnEven (f ∘ g) := by
  intro x
  dsimp
  calc f (g x)
    _= f (-g x) := by rw [ef]
    _= f (g (-x)) := by rw [og]

example (ef : FnEven f) (og : FnOdd g) : FnEven (f ∘ g) := by
  intro x
  dsimp
  calc f (g x)
    _= f (-g x) := by rw [ef]
  rw [og]

example (ef : FnEven f) (og : FnOdd g) : FnEven (f ∘ g) := by
  intro x
  dsimp
  rw [ef, og]

but did not need neg_neg, maybe there is a difference in definition?

[Zihao Zhang]

(deleted)