Zulip Chat Archive

Stream: Is there code for X?

Topic: finset.fold of option.lift_or_get


view this post on Zulip Eric Wieser (Oct 23 2020 at 17:08):

Are there any lemmas to help me make progress on this goal?

import data.finset.fold

open finset

variables {α β : Type*} (s : finset β) (f : α  α  α) (g : α  β) [is_associative α f] [is_commutative α f]

instance : is_associative β (equiv.arrow_congr g (equiv.arrow_congr g g) f) :=
λ x y z, by simp [@is_associative.assoc _ f _ _ _ _]⟩

instance : is_commutative β (equiv.arrow_congr g (equiv.arrow_congr g g) f) :=
λ x y, by {simp, rw [@is_commutative.comm _ f _ _ _]}⟩

example : (finset.fold (option.lift_or_get f)
            none (some  g.symm) s).map g
        = (finset.fold (option.lift_or_get (equiv.arrow_congr g (equiv.arrow_congr g g) f))
            none some s) :=
begin
  simp,
  sorry
end

Should those is_associative and is_commutative instances be in mathlib?

view this post on Zulip Eric Wieser (Oct 23 2020 at 17:56):

I suppose a likely useful building block would be:

def option_congr (e : α  β) : option α  option β :=
{ to_fun := option.map e,
  inv_fun := option.map e.symm,
  left_inv := λ x, by cases x; simp,
  right_inv := λ x, by cases x; simp, }

does that exist?

view this post on Zulip Yakov Pechersky (Oct 23 2020 at 18:01):

Is there the automatic construction of a equiv of set.inj_on?

view this post on Zulip Yury G. Kudryashov (Oct 23 2020 at 19:59):

docs#equiv.set.image_of_inj_on

view this post on Zulip Yury G. Kudryashov (Oct 23 2020 at 20:00):

(open data/equiv/basic, search for inj_on)

view this post on Zulip Eric Wieser (Oct 23 2020 at 20:04):

@Yakov Pechersky, can you explain the link between your question and mine?

view this post on Zulip Yakov Pechersky (Oct 23 2020 at 20:09):

Since option.some is injective, you have that (handwavy notation) α ≃ option.some '' α, then transitively with β, then identify none with each other.

view this post on Zulip Yakov Pechersky (Oct 23 2020 at 20:10):

Which is what your explicit structure does. I was wondering if there was shorthand for it.


Last updated: May 17 2021 at 15:13 UTC