Zulip Chat Archive

Stream: general

Topic: formulating continuity lemmas


Oliver Nash (Nov 05 2021 at 11:33):

@Floris van Doorn I was just looking at your remarks here https://leanprover.zulipchat.com/#narrow/stream/303200-sphere-eversion/topic/formulating.20continuity.20lemmas as well as the corresponding library note.

Oliver Nash (Nov 05 2021 at 11:34):

For example, should we therefore add the following:

import topology.algebra.module

variables {α β M : Type*} [topological_space α] [topological_space β] [topological_space M]
variables {f g : α  β} (hf : continuous f) (hg : continuous g) (t : M)

@[simp] lemma continuous_add' [has_add β] [has_continuous_add β] :
  continuous (f + g) :=
(@continuous_add β _ _ _).comp $ hf.prod_mk hg

@[simp] lemma continuous_sub' [has_sub β] [has_continuous_sub β] :
  continuous (f - g) :=
(@continuous_sub β _ _ _).comp $ hf.prod_mk hg

@[simp] lemma continuous_neg' [add_group β] [topological_add_group β] :
  continuous (-f) :=
continuous_neg.comp hf

@[simp] lemma continuous_smul' [has_scalar M β] [has_continuous_smul M β] :
  continuous (t  f) :=
(@continuous_smul M β _ _ _ _).comp (continuous_const.prod_mk hf)

Oliver Nash (Nov 05 2021 at 11:37):

Oh wait, I think I'm being silly. Ignore!

Eric Wieser (Nov 05 2021 at 11:37):

Why is that question silly?

Oliver Nash (Nov 05 2021 at 11:37):

Well for one thing, I had forgotten that we have docs#continuous.add etc

Eric Wieser (Nov 05 2021 at 11:38):

Oh, I thought your question was about using (λ x, f x + g x) vs f + g in the statement.

Oliver Nash (Nov 05 2021 at 11:38):

Nope!

Floris van Doorn (Nov 05 2021 at 12:02):

Yeah, we have the versions like docs#continuous.add. I don't think it matters too much whether we formulate with (λ x, f x + g x) vs f + g (that distinction matters for rw and simp, but these continuity proofs are usually proven using term-mode)

Reid Barton (Nov 05 2021 at 12:19):

I think continuity uses the reducible transparency level by default, in which case you would want the lemma statement to syntactically match whatever you have, which is most often the form with the lambda

Oliver Nash (Nov 05 2021 at 12:22):

Is this a feature of a limitation of continuity?

Floris van Doorn (Nov 05 2021 at 12:33):

Probably a necessary feature. Otherwise it would spend too much time unfolding definitions.


Last updated: Dec 20 2023 at 11:08 UTC