how to define a set?

Stream: lean4

[max]

variable (a b : P)
def s : Set P := {a, b}
#check s --{P : Type u_6} → P → P → Set P

is there a way to define s to be of type Set P instead of the function to Set P?
or is it not allowed?

[Edward van de Meent]

unfortunately, no. if you want to talk about the set containing a and b, you could add (s:Set P) (hs: \all c,c \in s \iff (c = a \or c = b))...

[Ruben Van de Velde]

What? Your s is a definition that takes two values of type P and gives you the set that contains them both. What do you want it to do, if not that?

[Edward van de Meent]

i'm guessing have s:Set P

[Ruben Van de Velde]

You could use {a b : P} to make them implicit, but I suspect that's not what you're after

[Kyle Miller]

Here's one of the ways you can work with fixed parameters across multiple definitions:

structure MyTheory (P : Type _) where
  (a b : P)

variable (t : MyTheory P)
def MyTheory.s : Set P := {t.a, t.b}

#check t.s
/-
t.s : Set P
-/

[Kyle Miller]

You can also make this structure a class if that's appropriate.

[Kyle Miller]

class MyTheory (P : Type _) where
  (a b : P)
open MyTheory

variable [MyTheory P]
def MyTheory.s : Set P := {a, b}

#check (s : Set P)
/-
s : Set P
-/

[Daniel Weber]

You can also do

variable {P : Type*} (a b : P)

local notation "s" => (insert a (singleton b) : Set P)

#check s