Stream: new members

Topic: Proving from optional parameter

Abhimanyu Pallavi Sudhir (Nov 13 2018 at 16:21):

How do I fill in the sorry?

example (c : ℝ) (f : ℝ → ℝ) (g : ℝ → ℝ := λ (x : ℝ), f (2 * c - x)) :  ∀ x, g x = f (2 * c - x) := sorry


Presumably I need to intro and input an x into g somehow -- but how? I know the specific example can be rewritten in a way that makes the proof by assumption, but this situation cropped up in another proof.

Chris Hughes (Nov 13 2018 at 16:25):

I don't think this is true. The := notation for g, just assigns a default value to g, if the user doesn't specify one when using the lemma, but you still have to prove for any g, since the user can override the default and use whatever value for g they like when using the lemma.

Kevin Buzzard (Nov 13 2018 at 17:21):

Maybe you want let g := ... in ...?

Chris Hughes (Nov 13 2018 at 17:33):

If you have let g := something in some proof, you can prove g = something with rfl.

Last updated: May 11 2021 at 00:31 UTC