Zulip Chat Archive

Stream: new members

Topic: function on product


view this post on Zulip Nicolò Cavalleri (Jun 18 2020 at 12:02):

Is there somewhere in Mathlib where I can find very primitive results on functions such that fxg \comp hxe = (f \comp h) x (g \comp e) where all functions have different domains and codomains exept from the obvious ones which need to be equal to make the equation work? It's not hard to prove it by myself but it would be cool to know if all these results are in Mathlib as I cannot really locate them. (I know the product function is written in Lean with λ abstraction but it was too long to write it with lean notation)

view this post on Zulip Scott Morrison (Jun 18 2020 at 12:08):

Do you know how to use library_search?

view this post on Zulip Scott Morrison (Jun 18 2020 at 12:10):

There are four strategies for finding statements in mathlib:

  1. learn the #naming scheme
  2. use library_search (sometime it helps to write a separate example with the statement you're after)
  3. ask here
  4. meander around in the source code!

view this post on Zulip Jalex Stark (Jun 18 2020 at 13:32):

I think following those more-or-less in order is good. In particular, by the time, you get to 3, you'll have an example that you can post with your question.

view this post on Zulip Kevin Buzzard (Jun 18 2020 at 13:34):

@Nicolò Cavalleri I would encourage you to formalise your questions (i.e. actually post a piece of working code with a sorry and say "what is this precise function called"). If you do that, you get much more efficient answers, and often, using library_search, you can even find out the answers yourself.

view this post on Zulip Nicolò Cavalleri (Jun 18 2020 at 14:40):

I am looking in Mathlib for lemmas of the kind:

lemma comp_of_prod_eq_prod_of_comp {A : Type*} {B : Type*} {C : Type*} {D : Type*} {E : Type*} {F : Type*}
(f : A  B) (g : C  D) (h : B  E) (k : D  F) :
(λ x : B × D, (h x.fst, k x.snd))  (λ x : A × C, (f x.fst, g x.snd)) = (λ x : A × C, ((h  f) x.fst, (k  g) x.snd)) :=
by refine rfl

library_search suggests refine rfl, but that is a tactic and does not point anywhere in mathlib. I am also wondering if there is a convenient notation for product of functions such as (λ x : A × C, (f x.fst, g x.snd))

view this post on Zulip Kenny Lau (Jun 18 2020 at 14:42):

rfl means "this is true by definition"

view this post on Zulip Kevin Buzzard (Jun 18 2020 at 14:46):

Not everything which is true by definition has a name in mathlib

view this post on Zulip Kevin Buzzard (Jun 18 2020 at 14:47):

Product function -- good question!

view this post on Zulip Nicolò Cavalleri (Jun 18 2020 at 14:51):

Does also refine rfl mean it is true by definition? The point is that if the goal is the rhs of = in the above lemma, exact lhs seems not to work, even if this is a simplification of my lemma so I am not entirely sure. That is why I needed to write the lemma separately

view this post on Zulip Bryan Gin-ge Chen (Jun 18 2020 at 14:52):

You should be able to replace by refine rfl with just rfl. refine without any underscores just does the same thing as exact.

view this post on Zulip Scott Morrison (Jun 18 2020 at 14:53):

This probably counts as a bug inlibrary_search that it doesn't just print rfl here...

view this post on Zulip Scott Morrison (Jun 18 2020 at 14:54):

I should also have library_search defer the solve_by_elim round until after the "only unfold reducible stuff" round...

view this post on Zulip Bryan Gin-ge Chen (Jun 18 2020 at 14:54):

Sometimes you have to use change to change the goal into something defeq before Lean will accept a proof of that via exact.

view this post on Zulip Johan Commelin (Jun 18 2020 at 14:54):

Scott Morrison said:

This probably counts as a bug inlibrary_search that it doesn't just print rfl here...

Well... then "Try this" would also have to replace the by...

view this post on Zulip Nicolò Cavalleri (Jun 18 2020 at 17:13):

What if I wanted to define (λ x : A × C, (f x.fst, g x.snd)) to be f.prod g? I think I could probably do it but I am a bit lost on what would be the standard way to do it

view this post on Zulip Johan Commelin (Jun 18 2020 at 17:19):

@Nicolò Cavalleri This is "difficult" to achieve, because functions are such a basic notion that there is no good dot notation for them at the moment.

view this post on Zulip Johan Commelin (Jun 18 2020 at 17:19):

You could get function.prod f g though

view this post on Zulip Nicolò Cavalleri (Jun 18 2020 at 17:22):

Johan Commelin said:

You could get function.prod f g though

Are you suggesting to define function.prod? Or does it exist already? (In case my Lean says it does not exist!)

view this post on Zulip Patrick Massot (Jun 18 2020 at 17:36):

This is prod.map.

view this post on Zulip Johan Commelin (Jun 18 2020 at 17:39):

Aah, I didn't pay attention to the maths...

view this post on Zulip Johan Commelin (Jun 18 2020 at 17:41):

@Nicolò Cavalleri function.prod (following current [informal?] naming conventions) would mean f : A → B, g : A → C, and then function.prod f g : A → B × C, the natural map \lam x, (f x, g x).

view this post on Zulip Johan Commelin (Jun 18 2020 at 17:41):

I think prod.map, which is what you want, already exists in mathlib.


Last updated: May 09 2021 at 19:11 UTC