How to define the set of all functions between two sets?

Stream: new members

[Justus Willbad]

I want to do algebra in Lean for formulating some simple new mathematical theorems. But I don't yet know the syntax and commands of Lean.

How can I formulate the following mathematical objects, the theorem and its proof in Lean?

Let
$X,Y$ sets,
$X_1\subseteq X$,
$Y_1\subseteq Y$,
$F$ the set of all functions out of $X$ into $Y$,
$F_1=\{f\in F\ |\ \forall x_0((x_0\in\text{dom}(f))\land (x_0\in X_1))\colon f(x_0)\in Y_1\}$.

Theorem:
$(\exists f\in F)\land(\exists x_0(x_0\in\text{dom}(f))\land(f(x_0)\notin Y_1))\implies f\notin F_1$

Until now, I have only

import Mathlib
variable (X : Type*)
variable (Y : Type*)
variable (X1 : Set X)
variable (Y1 : Set Y)

but don't know how to proceed.

[Daniel Weber]

Is F1 docs#Set.MapsTo ?

[Justus Willbad]

I don't know how to use things like X x Y, Set.MapsTo and Set.powerset.

[Eric Wieser]

What exactly does "A function in $X \times Y$" mean?

[Eric Wieser]

Does it mean functions from $X$ to $Y$? Or functions from $X \times Y$ to $X \times Y$?

[Daniel Weber]

What is $\operatorname{dom}(f)$? Isn't that always $X$?

[Eric Wieser]

(deleted)

[Daniel Weber]

Is this what you want?

import Mathlib
variable (X : Type*)
variable (Y : Type*)
variable (X₁ : Set X)
variable (Y₁ : Set Y)

example (f : X → Y) (h : ∃ x₀ ∈ X₁, f x₀ ∉ Y₁) : ¬Set.MapsTo f X₁ Y₁ := by
  intro hf
  obtain ⟨x, hx⟩ := h
  exact hx.2 <| hf hx.1

[Justus Willbad]

I corrected it: it is the set of all functions out of the set $X$ into the set $Y$.

[Justus Willbad]

Does

f : X → Y

mean $f\colon X\to Y$, or $X\supseteq\tilde{X}\to\tilde{Y}\subseteq Y$?

[Notification Bot]

This topic was moved here from #maths > How to use cross product and power set and make my proof? by Oliver Nash.

[Oliver Nash]

I'm afraid I don't quite know what is being asked but perhaps this may help:

import Mathlib

variable (X Y : Type*)

-- The type of functions `X → Y`
#check X → Y

-- The Cartesian product of two types:
#check X × Y

[Oliver Nash]

We also have a great resource which should help: https://leanprover-community.github.io/mathematics_in_lean/C01_Introduction.html

[Dan Velleman]

@Justus Willbad Note that in Lean, functions are not sets of ordered pairs. So you'll have to decide whether you want to state your theorem as a theorem about a function $f$ from $X$ to $Y$, in which case you can't treat $f$ as a set of ordered pairs, or as a theorem about a set $f$ of ordered pairs, in which case you can't treat $f$ as a function from $X$ to $Y$.

[Dan Velleman]

In response to one of your questions: f : X → Y means that f is a function from X to Y. It is not a function from a subset of X to a subset of Y. If a has type X, then f a has type Y. But f is not a set of ordered pairs, so you can't say that (a, f a) is an element of f.

[Justus Willbad]

How can I define the set of all functions $f_i\colon X\supseteq X_i\to Y_i\subseteq Y$ for all $f_i$?

[Dan Velleman]

You could do this:

def part_func_graphs (X Y : Type) : Set (Set (X × Y)) :=
  {f : Set (X × Y) | ∀ (x : X) (y1 y2 : Y),
    (x, y1) ∈ f ∧ (x, y2) ∈ f → y1 = y1}

According to this definition, if f ∈ part_func_graphs X Y then f is a set of ordered pairs, and in set theory it would be considered to be a function from a subset of X to a subset of Y. But in Lean, it is not a function, so you can't use function notation with f. So, for example, if a has type X and b has type Y then you can write (a, b) ∈ f, and you might think of that as meaning that b is the result of applying f to a, but you can't write b = f(a), because Lean will not recognize f as a function.

[Edward van de Meent]

Justus Willbad said:

How can I define the set of all functions $f_i\colon X\supseteq X_i\to Y_i\subseteq Y$ for all $f_i$?

here's another approach:

import Mathlib
set_option autoImplicit false

variable {X Y ι: Type*} (X' : ι → Set X) (Y' : ι → Set Y)

def subset_funs := (i:ι) × (X' i → Y' i) -- it's actually a type rather than set, but to get a set out of this you can just use `Set.univ`

[Matt Diamond]

Justus Willbad said:

How can I define the set of all functions $f_i\colon X\supseteq X_i\to Y_i\subseteq Y$ for all $f_i$?

import Mathlib

variable {X Y : Type*} {X_ : ℕ → Set X} {Y_ : ℕ → Set Y}

-- the type of all functions from X_i to Y_i
def f (i : ℕ) := X_ i → Y_ i

-- the set of all functions from X_i to Y_i
def f' (i : ℕ) := @Set.univ (X_ i → Y_ i)

(This uses ℕ as the index type, but you could also use a generic type as in Edward's solution above.)

Edit: I wonder if some of the confusion here is around trying to represent a function with an ambiguous domain. There's no need for a $dom(f)$ function in Lean (outside of partial functions) because the domain is guaranteed by the function's type. Are you trying to prove something about partial functions?

This feels like it might be an #xy problem...

Edit 2: This is closer to the wording of your question but I'm still not sure this is actually what you want:

import Mathlib

set_option autoImplicit false

variable {X Y : Type*} (X_ : ℕ → Set X) (Y_ : ℕ → Set Y)

-- a family of partial functions from X_i to Y_i
def F (i : ℕ) := { f : X →. Y | f.Dom = X_ i ∧ f.ran = Y_ i}

example
  (i : ℕ) (f : X →. Y)
  (x : X) (hx : x ∈ f.Dom)
  (hy : (f x).get hx ∉ Y_ i)
  : f ∉ F X_ Y_ i :=
by
  rw [F, Set.nmem_setOf_iff, not_and_or]
  right
  contrapose! hy
  rw [← hy, PFun.ran, Set.mem_setOf]
  use x
  exact Part.get_mem _

[Justus Willbad]

Matt Diamond schrieb:

I wonder if some of the confusion here is around trying to represent a function with an ambiguous domain. There's no need for a $dom(f)$ function in Lean (outside of partial functions) because the domain is guaranteed by the function's type. Are you trying to prove something about partial functions?

A set of functions with individual domains from $X$ is meant. Because the individual domain of a considered single function $f$ isn't known, I used the term $\text{dom}(f)$.
I had expected that Lean can translate nearly all terms and concepts of basic pure mathematics, that means also the identity of functions and sets of ordered pairs.

[Matt Diamond]

I had expected that Lean can translate nearly all terms and concepts of basic pure mathematics

It certainly can... if what you're trying to do requires that the specific domain of a function is unknown then perhaps partial functions are what you're looking for.

Relevant docs: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/PFun.html

[Kevin Buzzard]

The identification between functions and certain sets of ordered pairs as an equality is not a concept of basic pure mathematics, this is an artifact of what happens when mathematics is implemented in set theory. Lean is a functional programming language, and functions in lean are an undefined foundational concept, just like sets are an undefined foundational concept in set theory. In set theory, functions are defined in terms of sets. In Lean, sets are defined in terms of functions and the identification between functions and certain sets of ordered pairs is merely a bijection between two different things rather than being true by definition. Lean's foundations are type theory, not set theory.

You should not confuse mathematical concepts (like sets and functions) with implementation details which are foundation-specific (e.g. thinking that a function is a collection of ordered pairs).

[Kevin Buzzard]

An analogous situation would be if someone who was brought up on the type-theoretic foundations of mathematics started to use a set-theory-based theorem prover and incorrectly expected that a subset of a set X was equal to a function from X to the collection of true-false statements (sending the elements of the subset to "true" and the things not in the subset to "false"). The set theorists would point out that that these two concepts were not equal in set theory, but were merely in canonical bijection. In type theory these two concepts are identical. However we cannot deduce from this that the set-theory prover is not capable of handling "a concept of basic pure mathematics", because this is merely the implementation of sets in type theory.

[Justus Willbad]

I read somewhere "Set" in Lean means "subset". But now I read in the Lean documentation that it means "set".
I have to correct my code therefore to:

import Mathlib
variable (α β : Type*)
variable (X : Set α)
variable (Y : Set β)

But how can I create the variable $X_1\subseteq X$?

[Ruben Van de Velde]

That would also be a Set \a with h : X1 \subset X

[Edward van de Meent]

in lean, we tend to only consider sets as subsets of "master sets". That is, X : Set α really means X is a set that is a subset of the "master set" α : Type*. Depending on your situation, when you want to express $X \subset Y$, if you don't need to consider sets much larger than $Y$, you'd choose Y : Type* to be a "master set", and have X:Set Y be an arbitrary subset. on the other hand, if you need to have a larger set than $Y$ exist, you can do as Ruben suggested and declare X Y : Set α along with h : X ⊆ Y

[Kevin Buzzard]

Lean has two distinct things which the set theorists call sets -- one is types (an abstract collection of stuff) and one is subsets (of a fixed "master set" as Edward calls it, although a better term would be a "master type"). The collections of stuff are called X : Type and the subsets of X are called U : Set X but note that U is a term, not a type, so X and U behave differently in Lean's foundations for mathematics. If you're thinking set-theoretically then this is quite a good way to get confused about the basics here, because neither of these concepts (types, subsets) are a perfect fit for everything which a set theorist thinks about when they talk about sets (some of their sets are types and others are subsets); there is an art to doing the translation, and I would not recommend that you start focussing on this subtlety if you are a beginner to type theory, because you are quickly going to run into more statements which you might think are basic principles of mathematics but which turn out to be basic principles of set theory, and which might add to the confusion. In type theory, distinct types are always disjoint, for example.

[Justus Willbad]

How can I define X and X1 so that
#check X1 ⊆ X
gives no error?

[Ruben Van de Velde]

Backticks go the other way around

[Ruben Van de Velde]

import Mathlib

variable {α : Type*} {X X1 : Set α}

#check X1 ⊆ X

[Justus Willbad]

Both

#check X1 ⊆ X
#check X ⊆ X1

give no error, they give the type of the expression. That's not what I want.

How can I define in Lean that X1 is a subset of X and how can I check this?

[Matt Diamond]

Are you talking about a proof where you have a set X and you'd like to say "let X1 be an arbitrary subset of X"? Or is X1 defined in some other way?

[Matt Diamond]

If you're talking about a case where you want to prove something using the assumptions that you have a set X and a subset X1, then we would list those assumptions as arguments to the proof, in which case there's no need to "check" them since we've just provided proofs that they're true

something like:

theorem myTheorem {α : Type*} {X X1 : Set α} {h : X1 ⊆ X} : ... := sorry

with ... replaced by the proposition you're trying to prove

[Matt Diamond]

if you want to prove several different theorems about these sets, then the most common way to do this is to introduce them using the variable keyword, like so:

import Mathlib

variable {α : Type*} {X X1 : Set α} {h : X1 ⊆ X}

theorem myTheorem : ... := by
  -- here we have access to X, X1, and the proof that X1 is a subset of X
  sorry

[Justus Willbad]

I simply want to translate my mathematical objects and theorem from my first question into Lean and want to get a proof.
I expect I have to define a variable $X1$ with $X1\subseteq X$ and to define a variable $F$ that is the set of all functions out of $X$ into $Y$.
If $Y=X$, then $F$ is the set of all functions in $X$, e. g. in the complex numbers.

Is there no other solution than to define a new variable h?

h : X1 ⊆ X

[Kyle Miller]

Justus Willbad said:

But I don't yet know the syntax and commands of Lean.

Justus Willbad said:

I don't know how to use things like X x Y, Set.MapsTo and Set.powerset.

I would suggest reading Mathematics in Lean https://leanprover-community.github.io/mathematics_in_lean/index.html

There's also a list of learning resources kept on the community website: https://leanprover-community.github.io/learn.html

https://adam.math.hhu.de/#/ has a "set theory game" that's like the Natural Number Game.

[Alex Meiburg]

It may be easier if you explain a bit what you'd like to prove, and then people can give more precise guidance on how to state (and then, prove) this in Lean. I tried reading your first message a couple times over, and - as written in English - it looks like a false theorem to me. You say,

Justus Willbad said:

$(\exists f\in F)\land(\exists x_0(x_0\in\text{dom}(f))\land(f(x_0)\notin Y_1))\implies f\notin F_1$

Now I'm not sure if you mean
$(\exists ...)\land(... \implies ...)$
or
$\exists f \textrm{ such that } (f \in F (\land ... \implies ...))$
You might also mean something like
$((\exists ...)\land ...) \implies ...$
but then you have $f$ outside if the exists, and so I'm not sure what it's referring to.

The first option is an incorrect theorem. The statement $(\exists f\in F)$ does not always hold. If $Y$ is the empty set, then there can't be any functions from $X$ into $Y$, so there is no $f \in F$. So that's not a true statement.
The second one fails for the same reason. There doesn't always exist an $f \in F$.
And the third one is syntactically off.

Can you explain a bit more what exactly you want to show?

[Justus Willbad]

Theorem:
If there exist an $f\in F$ and an $x_0\in\text{dom}(f)$ so that $x_0\in X_1$ and $f(x_0)\notin Y_1$ then $f\notin F_1$.

I think I need to define, like in mathematics, all the mathematical objects in question first, formulate the theorem then and the proof at last.

[Dan Velleman]

Perhaps the theorem you are trying to state is:

example (X Y : Type) (X1 : Set X) (Y1 : Set Y)
    (F1 : Set (X → Y)) (f : X → Y) (x0 : X)
    (h1 : F1 = {f : X → Y | ∀ x ∈ X1, f x ∈ Y1})
    (h2 : x0 ∈ X1) (h3 : f x0 ∉ Y1) : f ∉ F1

But I agree with Kyle: before you can prove this, you need to learn how to use Lean. Kyle has pointed you toward some good learning resources.

[Alex Meiburg]

Here are a few ways to state your theorem:

variable (X Y : Type*) (X1 : Set X) (Y1 : Set Y)

theorem your_theorem (f : X → Y) (x₀ : X) (hx₀ : x₀ ∈ X1) (hfx₀ : f x₀ ∉ Y1) :
    let F₁ := { f : X → Y | ∀ x₀, x₀ ∈ X1 → f x₀ ∈ Y1 };
    f ∉ F₁ := by
  sorry

theorem your_theorem (X Y : Type*) (X1 : Set X) (Y1 : Set Y) (f : X → Y) (x₀ : X1) (h : f x₀ ∉ Y1) :
    f ∉ { g : X → Y | ∀ (x₀ : X1), g x₀ ∈ Y1 } := by
  sorry

This one has four sets that live in the same universe U. The funny ⟨x₀, hX1 x₀.2⟩ is saying: okay, to be able to plug x₀ into f, we need to show that it's in X. We are given that x₀ is in X1. So we combine the fact that x₀ is in X1 (which is x₀.2) with the fact that X1 is a subset of X (which is hX1) and this gives us a proof, hX1 x₀.2. Then the combined value ⟨x₀, hX1 x₀.2⟩ wraps the value x₀ together with its proof that it's in X, so that we can plug it into f.

variable (U : Type*) --The universe that all of our sets, X and Y, live in

variable (X Y X1 Y1 : Set U) (hX1 : X1 ⊆ X) (hY1 : Y1 ⊆ Y)

theorem your_theorem (f : X → Y) (x₀ : X1) (h : ((f ⟨x₀, hX1 x₀.2⟩) : U) ∉ Y1) :
    f ∉ { g : X → Y | ∀ (x₀ : X1), (g ⟨x₀, hX1 x₀.2⟩ : U) ∈ Y1 } := by
  sorry

This last one just does everything in terms of the base universe, without any real typing:

variable (U : Type*) --The universe that both of ours sets, X and Y, live in

variable (X Y X1 Y1 : Set U) (hX1 : X1 ⊆ X) (hY1 : Y1 ⊆ Y)

variable (f : U →. U) (hf : f.Dom = X) (hf' : f.image f.Dom = Y)

--The notation U →. U means that f is a function from U to U, but not necessarily
-- a total function; its domain may be smaller than U. Then we add the hypothesis that the
-- domain of f is exactly equal to the set X.

theorem your_theorem (x₀ : U) (hx₀ : x₀ ∈ X) (h : (f x₀).get (by rwa [← hf] at hx₀) ∉ Y) :
    f ∉ { g : U →. U | (g.Dom = X) ∧ (g.image g.Dom = Y) ∧ ∀ (x₀ : U), (g x₀).get (sorry) ∈ Y1 } := by
  sorry

(I cheated a little on the last one, trying to make it more readable.)

[Alex Meiburg]

I agree about learning it first, but I also think that (if you're used to set theory) then trying to learn by doing the 'simple' math makes sense as an attempt. But, yes, it's maybe counterintuitive but the 'fundamentals' are not the easiest place to get started, because the real basics of systems of math can be different, while the consequences are essentially the same.

[Justus Willbad]

Now I understood the code below.

import Mathlib
theorem MyTheorem (X Y : Type) (X1 : Set X) (Y1 : Set Y) (F1 : Set (X → Y)) (f : X → Y) (x0 : X)
(h1 : F1 = {f : X → Y | ∀ x ∈ X1, f x ∈ Y1}) (h2 : x0 ∈ X1) (h3 : f x0 ∉ Y1) : f ∉ F1 := by sorry

But how can I code the proof of contradiction where I assume the negation of the conclusion of the theorem ( ¬ (f ∉ F1) ) and Lean concludes that f(x) ∈ Y1 follows, what is a contradiction to the preconditions?

[Matt Diamond]

If you write intro h4 it will add h4 : f ∈ F1 to the proof state and update the goal to False. This is because f ∉ F1 is actually equivalent to f ∈ F1 → False. More generally a proof by contradiction can be started by using the by_contra tactic (or by_contra! to automatically push negations inward).

[Justus Willbad]

intro h4, intro or intro assumption work fine.
But how to proceed?

[Alex Meiburg]

Are you asking, just, how to write the proof? There are many possible ways to write this (fairly short) proof, and several people here could give you examples, but I'm guessing you want to learn how to write it yourself. I would suggest #tpil which will get you started on proof techniques

[Alex Meiburg]

As an example of a few very different solutions - spoilered in case you want to try more yourself first:

Four proofs

intro h
rw [h1] at h
exact h3 (h x0 h2)

contrapose! h3
simp [*] at h3
specialize h3 x0
apply h3
assumption

subst F1
dsimp
push_neg
use x0

exact (h3 <| x0 |> h1 ▸ . <| h2)

(This last one is kind of an absurd style, and obviously not very readable; it's a minimal way of writing the first proof, with intro, into a condensed form. I don't recommend it in practice, especially not when learning)

My point is that there are a lot of different ways to 'solve' this, the key thing is trying to see what works.

[Justus Willbad]

Thanks. Now I can work, play and learn with it.
It shows Lean seems suitable for my kind of mathematical problems.
Many many thanks to all of you.