Stream: new members
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
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
Last updated: May 11 2021 at 00:31 UTC