Zulip Chat Archive

Stream: Is there code for X?

Topic: Mapping finset.univ along an equiv gives finset.univ


view this post on Zulip Eric Wieser (Jan 03 2021 at 18:37):

This feels like it should exist somewhere:

lemma finset.univ_map_equiv {α β : Type*} [fintype α] [fintype β] (f : α  β) :
  (finset.univ : finset α).map f.to_embedding = (finset.univ : finset β) :=
sorry

view this post on Zulip Eric Wieser (Jan 03 2021 at 18:38):

Ah, library_search was just slow - docs#finset.univ_map_equiv_to_embedding


Last updated: May 16 2021 at 05:21 UTC