Dependent image

Stream: maths

[Sebastien Gouezel]

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 :=
begin
  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
end

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

[Scott Morrison]

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

[Mario Carneiro]

actually you only need set.range with that version