Stream: maths

Topic: Dependent image

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 :=
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 (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)

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