Finset from a Set of Fintype elements

Stream: new members

[Eric Zhao]

I've s : Type and an instance Fintype s. It seems like it should be possible to turn a X : Set s into a Finset s, but I can't seem to figure out how to do that. I might be missing something obvious here.

[Ruben Van de Velde]

Is that X.toFinset?

[Shanghe Chen]

Does this help? https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Finite.html#Set.Finite.toFinset

[Marcus Rossel]

docs#Set.toFinset

[Eric Zhao]

I had thought so, but Set.toFinset wants, in this case, a Fintype ↑X, but I've a Fintype s. I think ↑X is just { x : s // x ∈X }, so if I could get that this subtype is a Fintype that would work?

[Ruben Van de Velde]

I'd try to debug it if I had a #mwe

[Tom Kranz]

If your X has decidable membership, you can get a Fintype ↑X instance from https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Fintype/Basic.html#setFintype, otherwise (in which case you might not need computatbility anyway) you can magic one into existence with https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Fintype/Basic.html#Fintype.ofInjective and the injection from a set coerced into a type back into the original type, like so:

import Mathlib.Data.Fintype.Basic

example (t : Type) [Fintype t] (s : Set t) [DecidablePred (· ∈ s)]
: ∃ f : Finset t, ↑f = s := by
  have := setFintype s
  exact ⟨s.toFinset, s.coe_toFinset⟩

example (t : Type) [Fintype t] (s : Set t)
: ∃ f : Finset t, ↑f = s := by
  have : (λ e:↑s ↦ (e:t)).Injective := λ _ _ ↦ SetCoe.ext
  have := Fintype.ofInjective _ this
  exact ⟨s.toFinset, s.coe_toFinset⟩

[Kyle Miller]

@Tom Kranz Here are some simpler versions:

example (t : Type) [Fintype t] (s : Set t) [DecidablePred (· ∈ s)]
: ∃ f : Finset t, ↑f = s := by
  exact ⟨s.toFinset, s.coe_toFinset⟩

example (t : Type) [Fintype t] (s : Set t)
: ∃ f : Finset t, ↑f = s := by
  exact ⟨s.toFinite.toFinset, Set.Finite.coe_toFinset _⟩

[Kyle Miller]

Two ways to avoid decidability (while embracing noncomputability):

1. Use classical and s.toFinset

example (t : Type) [Fintype t] (s : Set t)
: ∃ f : Finset t, ↑f = s := by
  classical
  exact ⟨s.toFinset, s.coe_toFinset⟩

2. Use s.toFinite.toFinset

[Eric Zhao]

Thanks, I think this (the one with DecidablePred) is exactly what I wanted!