Zulip Chat Archive

Stream: new members

Topic: map filter_map join

Martin Dvořák (Jun 16 2022 at 12:07):

I am confused. Does my example hold?

example (a : list (list )) (f :   option ) :
  (list.map (list.filter_map f) a).join =
    list.filter_map f a.join :=

Eric Rodriguez (Jun 16 2022 at 12:16):

import data.list.join

example {α β} (l : list $ list α) (f : α  option β) :
  (l.map (list.filter_map f)).join = l.join.filter_map f :=
  induction l with h tl ih,
  { simp },
  { simp [list.filter_map_append, ih] },

Martin Dvořák (Jun 16 2022 at 14:13):

Don't we want to add it to mathlib alongside with the following theorem?

@[simp] theorem map_join (f : α  β) (L : list (list α)) :
  map f (join L) = join (map (map f) L) :=
by induction L; [refl, simp only [*, join, map, map_append]]

Notification Bot (Jun 16 2022 at 14:13):

Martin Dvořák has marked this topic as unresolved.

Eric Wieser (Jun 16 2022 at 15:58):

I don't know if the direction of those lemmas is right or whether they should be simp, but we should certainly have them in some form

Martin Dvořák (Jun 16 2022 at 18:06):

I am sorry for using a wrong word. The theorem map_join already exists in mathlib. I would like to add only one new theorem.

Martin Dvořák (Jun 16 2022 at 18:27):

Lemme PR it.

Martin Dvořák (Jun 16 2022 at 18:51):


Martin Dvořák (Jun 19 2022 at 19:40):

Should I move it to data/list/join as suggested?

Last updated: Dec 20 2023 at 11:08 UTC