Zulip Chat Archive

Stream: maths

Topic: Dependent image

view this post on Zulip Sebastien Gouezel (Apr 11 2020 at 19:59):

Is there a notation for dependent images (like '' for images), or even a name? I needed a lemma like

lemma finite_dependent_image
  {α : Type*} {β : Type*} {s : set α} (hs : set.finite s) (F : Π i  s, β) (t : set β)
  (H :  y  t,  x (hx : x  s), y = F x hx) : set.finite t :=
  let G : s  β := λ x, F x.1 x.2,
  have A : t  set.range G,
  { assume y hy,
    rcases H y hy with x, hx, xy,
    refine ⟨⟨x, hx, xy.symm },
  letI : fintype s := set.finite.fintype hs,
  exact set.finite_subset (set.finite_range G) A

and I didn't even find a nice way to express it.

view this post on Zulip Scott Morrison (Apr 12 2020 at 01:52):

Can you just talk about the usual '' image of the related function s -> β? (i.e. coerce s to a type)

view this post on Zulip Mario Carneiro (Apr 12 2020 at 01:58):

actually you only need set.range with that version

Last updated: May 14 2021 at 19:21 UTC