Set theory

Stream: lean4

[The-Anh Vu-Le]

Hi, I am trying to read through and recreate Mathlib's set theory for my self-learning, but I am stuck with a few errors. The code is

axiom MySet.{u} (α : Type u) : Type u

axiom MySet.mem.{u, v} {α : outParam (Type u)} {γ : Type v} :
  γ → α → Prop
notation:50 x:50 " ∈ " S:50 => MySet.mem S x
notation:50 x:50 " ∉ " S:50 => ¬ (x ∈ S)

axiom MySet.empty.{u} {α : Type u} : α
notation:max "∅" => MySet.empty

axiom MySet.not_mem_empty.{u} {α : Type u} :
  ∀ (x : α), x ∉ ∅

The error is at the x ∉ ∅ part of the last axiom. There are two, specifically,

don't know how to synthesize implicit argument 'γ'
  @mem α (?m.3742 x) ∅ x
context:
α : Type u
x : α
⊢ Type u_1

don't know how to synthesize implicit argument 'α'
  @empty (?m.3742 x)
context:
α : Type u
x : α
⊢ Type u_1

The problem goes away if I do something like x ∉ (∅ : MySet α) or even x ∉ (∅ : α). Is there a good way to go about this?

[Kevin Buzzard]

Mathlib has this problem too:

import Mathlib

example (α : Type) (x : α) : x ∈ ∅ := by sorry
/-
typeclass instance problem is stuck, it is often due to metavariables
  Membership α ?m.88
-/

[The-Anh Vu-Le]

Interesting. I was doing #check ∀ {α : Type} (x : α), x ∉ ∅ which worked, so I assumed it would work. I guess it cannot directly infer that ∅ should be treated as Set α, even though we have (x : α)?
Thanks anyway!

[Aaron Liu]

There are other things ∅ could be, such as Finset α or List α, so you need to specify that it is Set α.