easy finite set question

Stream: general

[Kevin Buzzard]

import data.set
example (X Y : Type) (C : set X) (HC : set.finite C) (f : C → Y) : set.finite (set.range f) := sorry

[Kevin Buzzard]

I see fintype_range, an instance proving that the range of a function with fintype domain is a fintype, but I have never worked with finite sets/types before. Should I be switching to and fro between finite sets and fintypes? Should I be letting type class inference and/or automation do the work for me? This stuff looks pretty easy in maths so hopefully isn't too painless here.

[Kenny Lau]

import data.set

local attribute [instance] classical.prop_decidable

example (X Y : Type) (C : set X) (HC : set.finite C) (f : C → Y) : set.finite (set.range f) :=
HC.rec $ λ HF, nonempty.intro $ @set.fintype_range _ _ _ f HF

[Kenny Lau]

import data.set

local attribute [instance] classical.prop_decidable

example (X Y : Type) (C : set X) (HC : set.finite C) (f : C → Y) : set.finite (set.range f) :=
let ⟨HF⟩ := HC in ⟨@set.fintype_range _ _ _ f HF⟩

[Kenny Lau]

import data.set

local attribute [instance] classical.prop_decidable

example (X Y : Type) (C : set X) (f : C → Y) : set.finite C → set.finite (set.range f)
| ⟨HF⟩ := ⟨@set.fintype_range _ _ _ f HF⟩

[Kevin Buzzard]

Thanks Kenny. I have spent all evening reducing the statement that Spec(R) is compact to the case of covers by a basis ;-)

[Kenny Lau]

nice