Zulip Chat Archive

Stream: new members

Topic: please help me


Zihao Zhang (Sep 13 2024 at 12:15):

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 (Sep 13 2024 at 12:15):

#backticks
#mwe

Derek Rhodes (Sep 13 2024 at 15:25):

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 (Sep 16 2024 at 12:11):

(deleted)


Last updated: May 02 2025 at 03:31 UTC