Sets and Types

Stream: new members

[ooovi]

Hi all!
I have A : Finset V and S : Finset { x // x ∈ A }, and I would like to obtain an S' : Finset V such that S' ⊆ A, and for x ∈ S' I have x ∈ S and vice versa. I'm having trouble even writing that down as a type, because of course the things in S' and S have different types:

def hmm {V : Type} {A : Finset V} (S : Finset { x // x ∈ A }) :
    ∃ S' : Finset V, S' ⊆ A ∧ (∀ x, x ∈ S' ↔ x ∈ S) := by sorry

Because it does not actually make sense to say x ∈ S, lean tells me failed to synthesize Membership V (Finset { x // x ∈ A }). So x ∈ S not quite what I want, but I'm not sure what is. A Bijection between S and S'? Will I need to write it myself or does it exist somewhere already and I'm just not seeing it?

So far, i have managed to prove a statement about a S' : Set V (not Finset) and the coercion of x, but that's not sufficient for my needs:

def hmm {V : Type} {A : Finset V} (S : Finset { x // x ∈ A }) :
    ∃ S' : Set V, S' ⊆ A ∧ (∀ x, ↑x ∈ S' ↔ x ∈ S) := by
  use { ↑x | x ∈ S }
  simp_all only [Subtype.exists, exists_and_right, exists_eq_right]
  constructor
  . intro _ xins
    exact xins.out.1
  · intro x
    simp

Any hints? Am I even making sense?

[Jihoon Hyun]

What you're trying to do is in the queue #19514 . If you're in a hurry, please check the implementation of it.

[Kevin Buzzard]

How did you end up with S in the first place? Usually my advice to students who get into this kind of situation is to look at which point they changed a term into a type (which for you is { x // x ∈ A }) and to see if there is a way of avoiding this (e.g. by not making S at all and instead directly making S' at the point where they made S). But sometimes it's unavoidable.

[ooovi]

It's the vertex set of a subgraph induced by A.