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):
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