Stream: Is there code for X?

Topic: finset.fold of option.lift_or_get

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?

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?

Yakov Pechersky (Oct 23 2020 at 18:01):

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

Yury G. Kudryashov (Oct 23 2020 at 19:59):

docs#equiv.set.image_of_inj_on

Yury G. Kudryashov (Oct 23 2020 at 20:00):

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

Eric Wieser (Oct 23 2020 at 20:04):

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

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.

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