Set operation with 2 inputs are not supported

Stream: new members

[Yunong Shi]

I have a function to compose two sets:

import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.Data.Matrix.Kronecker

def Qudit (d: Nat): Set (Matrix (Fin d) (Fin 1) ℂ) := {ψ | ψᴴ * ψ = 1}

def ComposedQudits (d1 d2: Nat) := {ψ ⊗ₖ φ| ψ ∈ Qudit d1 ∧ φ ∈ Qudit d2}

It complains unknown identifier ψ, φ.

If I only have 1 input, then the above works:

def ComposedQudits (d1: Nat) := {ψ + ψ | ψ ∈ Qudit d1}

If Qudit is a type, then the above also works:

structure Qudit2 (d: Nat) where
  ψ: Matrix (Fin d) (Fin 1) ℂ
  normalized: ψᴴ * ψ = 1

def ComposedQudits3 (d1 d2: Nat) := {ψ.1 ⊗ₖ φ.1| (ψ : Qudit2 d1) (φ: Qudit2 d2)}

I am wondering how to support the above use case (Qudit being Sets and having 2 inputs to Set operations)?

[Kyle Miller]

Does {ψ ⊗ₖ φ| (ψ ∈ Qudit d1) (φ ∈ Qudit d2)} work?

[Yunong Shi]

Kyle Miller said:

Does {ψ ⊗ₖ φ| (ψ ∈ Qudit d1) (φ ∈ Qudit d2)} work?

Yes, thank you :joy: . I thought ψ ∈ Qudit d1 and φ ∈ Qudit d2 are propositions and you need to And them

[Kyle Miller]

Yes, they are propositions, but they also have an interpretation as binders, so this is able to work.

[Yunong Shi]

Kyle Miller said:

Yes, they are propositions, but they also have an interpretation as binders, so this is able to work.

Yep, makes sense. Found those extended binder definitions in Mathlib/Init/Set.lean.