Zulip Chat Archive
Stream: Is there code for X?
Topic: product of surjective functions is surjective
Bernd Losert (Jan 27 2022 at 19:54):
I'm looking for a lemma that says that prod.map f g is surjective when f and g are, but I can't find one.
Adam Topaz (Jan 27 2022 at 19:55):
docs#function.surjective.prod_map
Adam Topaz (Jan 27 2022 at 19:55):
Do you know about https://leanprover-community.github.io/mathlib_docs/ ?
Bernd Losert (Jan 27 2022 at 20:04):
Ah, you found it. I guess I wasn't looking hard enough.
Bernd Losert (Jan 27 2022 at 20:05):
Yeah, I know about the docs. I was searching for prod.map in the function stuff, but I couldn't find anything.
Bernd Losert (Jan 27 2022 at 20:06):
Ah, that's in data.prod. No wonder I couldn't find it.
Bernd Losert (Jan 27 2022 at 20:07):
I know lean has a library_search tactic. Maybe I need to start using that to find stuff.
Last updated: Dec 20 2023 at 11:08 UTC