Finset of subtype 2

Stream: new members

[Gareth Ma]

Hi, how do I write this?

example {α : Type*} {p : α → Prop} {s : Finset α} (hs : ∀ x, p x) : Finset { x // p x } := by
  sorry

[Gareth Ma]

Wait I'm very sorry, I didn't realise there's a previous thread with the same name lol

[Notification Bot]

2 messages were moved here from #new members > Finset of subtype by Gareth Ma.

[Yaël Dillies]

s.map ⟨fun x ↦ ⟨x, hs x⟩, sorry⟩

[Notification Bot]

Gareth Ma has marked this topic as resolved.

[Notification Bot]

Gareth Ma has marked this topic as unresolved.

[Gareth Ma]

example {α : Type*} {p : α → Prop} {s : Finset α} (hs : ∀ x ∈ s, p x) [DecidablePred p] :
    Finset { x // p x } :=
  sorry

[Yaël Dillies]

s.attach.map ⟨fun x ↦ ⟨x, hs _ x.2⟩, sorry⟩

[Alex Brodbelt]

I ask here, but feel free to move this question to another thread:

I am trying to prove that a finset of a subtype is nonempty, I have constructed a term of the subtype but I have the strange issue that I cannot show it belongs to the Finset of the subtype, I would expect proving it belongs to the Finset would be straightforward just show it satisfies P, but it seems I must be stating something wrong or vacuous, because rw? just goes in loops and to my eyes does not provide anything useful and apply? does not do much good either.

This is the lemma I think should solve my problems.

lemma triv {P : ℕ → Prop} {s : Finset {p : ℕ // P p}} (x : ℕ) (hx : P x) : ⟨x, hx⟩ ∈ s := by
  sorry

[Ilmārs Cīrulis]

@Alex Brodbelt This can't be proved, because it's possible that ⟨x, hx⟩ doesn't belong to s.

For example, if s is empty or Finset.empty.

[Edward van de Meent]

indeed. the confusion might be coming from the precise meaning of s: Finset {p : Nat // P p}. It means "Let s be a finite set whose elements are naturals which satisfy P", not "Let s be be a finite set whose elements are precisely those naturals which satisfy P"

[Alex Brodbelt]

Oh I see, I was indeed misunderstanding what the type meant.

[亚历山大大帝]

(deleted)