Statement about set & subsets

Stream: new members

[Luke Hammer]

I want to formalize a proof of the following statement: "There exists a set S which is equal to the set of its finite subsets".
Although, I've found myself stuck at the very first step: formalizing the statement.

My attempts (two of which I show below) all fall to type mismatches, as Set t is a different type from t.

import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.Finite

theorem set_eq_own_finsets1 : ∃ (S : Set (Set α)) , S = {T : Set α | Set.Finite T ∧ T ⊆ S} := sorry
theorem set_eq_own_finsets2 : ∃ (S : Set α) , S = {T : Set α | Set.Finite T ∧ T ⊆ S} := sorry

How would I get around this? Should I use a different type instead of Set?

[Matt Diamond]

if you're trying to prove something about sets in the Set Theoretical sense (where the members of the sets are sets themselves and it's sets all the way down), then docs#ZFSet may be a better choice of type

[Matt Diamond]

though the tools for dealing with that kind of set are fairly limited... for example I don't think ZFSet.Finite is a thing (yet)

[Luke Hammer]

Ok cool, thanks for the info!