## Stream: general

### Topic: easy finite set question

#### Kevin Buzzard (Apr 15 2018 at 02:37):

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 (Apr 15 2018 at 02:39):

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 (Apr 15 2018 at 02:47):

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 (Apr 15 2018 at 02:48):

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 (Apr 15 2018 at 02:53):

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 (Apr 15 2018 at 02:53):

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 (Apr 15 2018 at 02:53):

nice

Last updated: May 18 2021 at 17:44 UTC