Working with functions on sets in ZFC

Stream: new members

[Moham Balfakeih]

Hello, I am taking an axiomatic set theory course and saw it as an opportunity to learn lean by formalizing some of the homework assignments using Mathlib.SetTheory.ZFC.

Without revealing the homework, I define A B : ZFSet and a function f : A → B (which then gets coerced to ↥A → ↥B). I then require the image of this function, so I attempted to use: ZFSet.image f A, however this does not work as f needs to be a function from ZFSet.{u} → ZFSet.{u}.

From my understanding, I think there's a bigger issue in defining a function like this since f is expected to take in elements of ↥A , but since A is a ZFSet it only contains ZFSets of a lower type universe. Is there an expected way to work with functions in ZFC that I'm not seeing? Mathlib.SetTheory.ZFC.Basic defines functions as a subset of the cartesian product of the domain and codomain by ZFSet.IsFunc, but I don't see how I can perform function application with this since it is of type ZFSet.

[Snir Broshi]

What's the specific problem? Can you create a #mwe ?

[Snir Broshi]

You might be looking for the range function rather than image:

import Mathlib.SetTheory.ZFC.Basic

noncomputable section

variable {A : ZFSet} {f : A → ZFSet}

def range_of_f : ZFSet := ZFSet.range f

[Moham Balfakeih]

I don't want to state the specific problem as this is a graded homework exercise.

I don't have much of an MWE I can form without actually defining the image (or coming up with some other problem I can formulate that requires the image), which I don't know how to.

import Mathlib.SetTheory.ZFC.Basic

theorem exercise: ∀ (A B : ZFSet) (f : A → B),  /- Some theorem that needs the image of f, e.g. the image of f is a subset of B, how would one represent the image of f? -/ := by sorry

[Snir Broshi]

If you're okay with using regular sets you can do:

import Mathlib

variable {α : Type} {A B : Set α} {f : A → B}

def range_of_f : Set B := Set.range f

[Moham Balfakeih]

Makes sense, I was hoping I could do this with ZFSet since the problems are explicitly in ZFC set theory

[Snir Broshi]

Yes but I believe ZFSet is more fit for a logic course rather than an introductory set theory course

[Snir Broshi]

Moham Balfakeih said:

I don't want to state the specific problem as this is a graded homework exercise.

I meant the specific problem you're having, not the exercise. It's hard to understand what you want exactly without knowing what you're going to do with it.
Can you perhaps make up some problem that has similar requirements to the homework?

[Dexin Zhang]

You can do something like def g : ZFSet → ZFSet := fun x => if hx : x ∈ A then f ⟨x, hx⟩ else ∅ (∅ can be replaced by any junk value) and then write ZFSet.image g A

[Moham Balfakeih]

I believe this is a similar enough problem, except in my original problem I want the domain of g to be the image of f. I then want to use that information to construct g (a problem I was planning on dealing with after I figured out how to get the image :sweat_smile: )

import Mathlib.SetTheory.ZFC.Basic

theorem bij_implies_bij: ∀ (A B : ZFSet) (f : A → B), Function.Bijective f
  → ∃ (g : B → A), Function.Bijective g := by
  unfold Function.Bijective Function.Injective Function.Surjective
  rintro A B f ⟨hfi,hfs⟩
  exists ... /- construction of g -/

[Moham Balfakeih]

Dexin Zhang said:

You can do something like def g : ZFSet → ZFSet := fun x => if hx : x ∈ A then f ⟨x, hx⟩ else ∅ (∅ can be replaced by any junk value) and then write ZFSet.image g A

With this I get the error failed to synthesize instance of type class Decidable (x ∈ A).

Full code:

import Mathlib.SetTheory.ZFC.Basic

variable {A B : ZFSet} {f : A → B}
def g : ZFSet → ZFSet := fun x => if hx : x ∈ A then f ⟨x, hx⟩ else ∅

[Aaron Liu]

you can use docs#ZFSet.range

[Aaron Liu]

but also I would suggest not using ZFSet at all and just using types

[Dexin Zhang]

Moham Balfakeih said:

With this I get the error failed to synthesize instance of type class Decidable (x ∈ A).

Then you can open Classical and write noncomputable def

[James E Hanson]

Aaron Liu said:

but also I would suggest not using ZFSet at all and just using types

The class is explicitly about ZFC.

[Moham Balfakeih]

Dexin Zhang said:

Moham Balfakeih said:

With this I get the error failed to synthesize instance of type class Decidable (x ∈ A).

Then you can open Classical and write noncomputable def

That still doesn't allow me to useZFSet.image as it can't synthesize the typeclass ZFSet.Definable₁ g

Full code:

import Mathlib.SetTheory.ZFC.Basic

open Classical

variable {A B : ZFSet} {f : A → B}

noncomputable def g : ZFSet → ZFSet := fun x => if hx : x ∈ A then f ⟨x, hx⟩ else ∅

noncomputable def image_of_g := ZFSet.image g A

[Moham Balfakeih]

Aaron Liu said:

you can use docs#ZFSet.range

That takes a function that goes from a type to a set though, while with my current implementation I would need something that goes from one type to another, with both of those types beingZFSet

[Dexin Zhang]

Moham Balfakeih said:

That still doesn't allow me to useZFSet.image as it can't synthesize the typeclass ZFSet.Definable₁ g

Yeah, unfortunately you need to do

noncomputable def image_of_g :=
  have := @Classical.allZFSetDefinable
  ZFSet.image g A

[Dexin Zhang]

I don't know why docs#Classical.allZFSetDefinable is not scoped instance

[James E Hanson]

You could make it an instance like this to avoid having to write that possibly multiple times:

import Mathlib.SetTheory.ZFC.Basic

noncomputable instance {n : ℕ} (F : (Fin n → ZFSet.{u}) → ZFSet.{u}) : ZFSet.Definable n F := Classical.allZFSetDefinable _

[Aaron Liu]

James E Hanson said:

Aaron Liu said:

but also I would suggest not using ZFSet at all and just using types

The class is explicitly about ZFC.

Seeing one of the examples of a "similar problem" #new members > Working with functions on sets in ZFC @ 💬 being a theorem in mathlib that is proved without any mention of ZFSet leads me to believe it is not specifically about ZFC.

[James E Hanson]

Aaron Liu said:

Seeing one of the examples of a "similar problem" #new members > Working with functions on sets in ZFC @ 💬 being a theorem in mathlib that is proved without any mention of ZFSet leads me to believe it is not specifically about ZFC.

Sure, the content of such a problem isn't specifically a ZFC thing (just as how it isn't specifically a Lean thing), but the point is that Moham's class is working in ZFC.

[Snir Broshi]

Every sensible math class works in ZFC, that doesn't mean we formalize using ZFC

[James E Hanson]

Moham Balfakeih said:

Hello, I am taking an axiomatic set theory course and saw it as an opportunity to learn lean by formalizing some of the homework assignments using Mathlib.SetTheory.ZFC.

Honestly, if you goal is to try to stay close to the formalism of your class, I'm not sure Lean is right proof assistant to be using. ZFSet is fairly incomplete and, at least for the moment, you really need to understand its implementation (e.g., the notion of pre-sets) in order to work with it. It might be easier to work with Metamath, Isabelle/ZF, or Mizar at the end of the day.

[Violeta Hernández]

pre-sets are an implementation detail I've wanted to get rid of for years now, maybe now is the time I finally open that PR

[James E Hanson]

Violeta Hernández said:

pre-sets are an implementation detail I've wanted to get rid of for years now, maybe now is the time I finally open that PR

How would you propose getting rid of pre-sets?

[Matt Diamond]

@James E Hanson I'm guessing it would be via docs#QPF as discussed in this thread: #mathlib4 > ZFSet and computability @ 💬

[Moham Balfakeih]

James E Hanson said:

Moham Balfakeih said:

Hello, I am taking an axiomatic set theory course and saw it as an opportunity to learn lean by formalizing some of the homework assignments using Mathlib.SetTheory.ZFC.

Honestly, if you goal is to try to stay close to the formalism of your class, I'm not sure Lean is right proof assistant to be using. ZFSet is fairly incomplete and, at least for the moment, you really need to understand its implementation (e.g., the notion of pre-sets) in order to work with it. It might be easier to work with Metamath, Isabelle/ZF, or Mizar at the end of the day.

Yeah that makes sense, I'll look into that, thanks for all the help!