Zulip Chat Archive

Stream: new members

Topic: Constructing Types


view this post on Zulip Chase Norman (Dec 23 2020 at 22:06):

I have an existing fintype X. I would like to produce a Type that has all of the elements of X except a given element x. Is such a construction possible? If so, what route could I take to prove that the resulting type is a fintype? Thanks.

view this post on Zulip Yakov Pechersky (Dec 23 2020 at 22:26):

One simple way would be

import data.fintype.basic

variables {α : Type*} [fintype α] [decidable_eq α] {a : α}

example : fintype {x // x  a} := by show_term {apply_instance}

/-
Try this: exact subtype.fintype (λ (x : α), x ≠ a)

-/

view this post on Zulip Yakov Pechersky (Dec 23 2020 at 22:27):

Without the decidable_eq, you don't have a decidable procedure for knowing whether two elements are the same or not, so you don't know if an element is really in your subtype.

view this post on Zulip Eric Wieser (Dec 23 2020 at 23:30):

But you can always use open_locale classical if you don't care about computably enumerating the values


Last updated: May 14 2021 at 21:11 UTC