Clunky and condition

Stream: new members

[VayusElytra]

Hello, I am working on the following relationship between sets of integers:

structure ExampleStruct where
  {S : Finset ℕ}

def ExampleRelation : ExampleStruct → ExampleStruct → Prop :=
  fun I J => ∃ d : (ℕ → Finset ℕ), ∀ N ∈ I.S, N = (∑ x ∈ (d N), x) ∧ ∀ N ∈ I.S, d N ⊆ J.S

The idea is that I and J are in a relationship if every element in the associated set to I can be expressed as a sum of elements of J's associated set. My function d only needs to map elements in I.S to the corresponding subset in J.S, so here it has too large a domain and codomain.

I think the condition ∀ N ∈ I.S, d N ⊆ J.S is clunky. It feels like this statement could just be integrated into the type of the codomain of d, but I haven't found anything too convincing so far. I have tried having d's codomain be Set J.S and Subtype J.S, but they create complications.

How would you write this properly?

[Bjørn Kjos-Hanssen]

This works and is maybe not too clunky(?):

import Mathlib.Data.Finset.Basic
import Mathlib.Algebra.BigOperators.Group.Finset

structure ExampleStruct where
  {S : Finset ℕ}

def ExampleRelation : ExampleStruct → ExampleStruct → Prop :=
  fun I J => ∃ d : I.S → Finset.powerset J.S,
    ∀ N : ℕ, (h : N ∈ I.S) →  N = ∑ x ∈ (d ⟨N,h⟩), x

[VayusElytra]

Thank you, this is indeed a lot better!

[Bjørn Kjos-Hanssen]

Basically, powerset takes care of the problem of turning a subset of a Finset into another Finset.