Zulip Chat Archive

Stream: general

Topic: easy finite set question


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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⟩

view this post on Zulip 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⟩

view this post on Zulip 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 ;-)

view this post on Zulip Kenny Lau (Apr 15 2018 at 02:53):

nice


Last updated: May 18 2021 at 17:44 UTC