Image of a set under relation

Stream: new members

[Andrew Lubrino]

I'm trying to prove that if a set A is a subset of B then the image of A under relation R is a subset of the image of B under relation R. I've got the code below:

import data.set
open set

variable {U : Type}
variables A B: set U
variable R : U → U → Prop

theorem subset_image : A ⊆ B → R '' A ⊆ R '' B :=
begin
  intros h1 x h2,
  simp at h2,
  rcases h2 with ⟨c, h3, h4⟩,
  sorry
end

According to mathlib, this is the notation for the image of a function, so I'm guessing the notation is the same for a relation. My x in this example is assigned U → Prop. Is this assignment correct? Am I using the right notation to prove what I'm looking to prove here? It doesn't feel like the right assignment, but I also wouldn't be able to give a reason that it would be wrong.

[Patrick Massot]

R is a function from U to functions from U to Prop. Hence the image of A is a set in U → Prop

[Patrick Massot]

This is clearly not what you want

[Patrick Massot]

I'm not even sure what you want to state

[Patrick Massot]

What do you mean by "image of a set under a relation"?

[Reid Barton]

Probably {b | \exists a, R a b}

[Patrick Massot]

Is it meant to generalize the case where R is the graph of a function?

[Patrick Massot]

You probably want to have a look at https://leanprover-community.github.io/mathlib_docs/logic/relation.html

[Andrew Lubrino]

I'm working through (Elias Zakon's Basic Mathematics)[http://www.trillia.com/dA/zakon-basic-us-one.pdf], so the below problem is page 20 of that book.

Prove the following: If A ⊆ B, then R[A] ⊆ R[B]

He uses the phrase 'image of A under a relation R'. Is his terminology and notation not standard?

[Andrew Lubrino]

If the notation is unfamiliar, he also gives the below definition

By definition, R[x] is the set of all R-relatives of x. Hence y ∈ R[x] means that y is an R-relative of x, i.e., that (x, y) ∈ R, which can also be written as
xRy. Thus the formulas (x, y) ∈ R, xRy and y ∈ R[x] are equivalent.

[Andrew Lubrino]

Oh didn't see that link. Let me look at that. Thank you!

[Kevin Buzzard]

The thing you wrote above does not correspond to your lean code. Maybe you want to write your own code for the image rather than using R '', which means something else (namely, the image of a set under a function)

[Andrew Lubrino]

Yes, that's what I was asking. Thanks very much. @Kevin Buzzard

Also, if no one even knows about this thing I'm talking about, it must be unimportant. I'm thinking I should skip these questions.

[Kevin Buzzard]

It's good lean practice doing this sort of thing

[Kevin Buzzard]

In fact you still haven't said what your question means; you only defined R[x] for x : U but in your question you have R[A] for A : set U. You can't do it in Lean until you've explained what the question means.

[Andrew Lubrino]

Yes, maybe you're right. I have been meaning to learn how to write definitions in Lean. I'd be writing a def right? I was thinking of using the below as an example, but obviously changing the definition to have the notation and content
(so basically it will only have the same structure as below, but none of the same content) from the example question (taken from Logic and Proof):

def reflexive (R : A → A → Prop) : Prop :=
∀ x, R x x

Is this the right direction? Would there be anything I could use to get that bracket notation, similar to what's in the practice example?

[Kevin Buzzard]

Let's get the definition first, before worrying about the notation. You still haven't told us the mathematical definition.

[Andrew Lubrino]

Okay, hold on let me find the definition in the book.

[Andrew Lubrino]

Okay, this is the first part, telling us what an R-relative is:

If R is a relation, and (x, y) ∈ R, then y is called an R-relative of x

and the second part is here:

The image of a set A under a relation R (briefly, the R-image of A) is the set of all R-relatives of elements of A.

so, putting the two together, I think a good definition would be the below:

{ y | \ex x \in A, R x y} where R is a relation

[Kevin Buzzard]

OK then, so it's

import data.set
open set

variable {U : Type}
variables A B: set U
variable R : U → U → Prop

-- the definition
def relation.image (A : set U) : set U := { y | ∃ x, x ∈ A ∧ R x y}

-- notation for the deiinition
notation R`[[`:1024 A`]]`:1024 := relation.image R A

-- the API for the definition
lemma relation.image_def (A : set U) (y : U) : y ∈ R[[A]] ↔ ∃ x, x ∈ A ∧ R x y :=
begin
  refl
end

theorem subset_image : A ⊆ B → R[[A]] ⊆ R[[B]] :=
begin
  -- over to you
  sorry
end

[Kevin Buzzard]

theorem subset_image : A ⊆ B → R[[A]] ⊆ R[[B]] :=
begin
  intro hAB,
  rw set.subset_def,
  intros y hy,
  rw relation.image_def at hy ⊢,
  cases hy with x hx,
  cases hx with hxA hRxy,
  use x,
  split,
  { rw set.subset_def at hAB,
    apply hAB,
    exact hxA },
  { exact hRxy }
end

theorem subset_image' : A ⊆ B → R[[A]] ⊆ R[[B]] :=
begin
  rintros hAB y ⟨x, hxA, hRxy⟩,
  exact ⟨x, hAB hxA, hRxy⟩,
end

[Andrew Lubrino]

Wow, that's amazing. Thanks so much. I want to start writing more of my own definitions in the future. I have two questions about this: 1) is there any way to keep these definitions in a different file and them import them like I import data.set? 2) I'm a total beginner. the definition I gave you above sounds right to me, but I'm honestly not sure. Is there any way to verify that my definition captures what the author really had in mind short of asking someone with more experience?

[Kevin Buzzard]

The only way to find out what the author had in mind was to read the book written by the author. Note however that based on the context Reid guessed something very close to this about an hour ago.

[Kevin Buzzard]

Importing definitions -- no problem at all. You can see me doing it in my undergraduate course here for example. Did you make a Lean project yet? If so, and if you're putting your files in /src, it should just work. In the example I link to, I am importing src/solutions/section02reals/sheet3.lean.

[Andrew Lubrino]

Yes, I have a Lean project up and running. I'm trying this now. I named the file relation_image.lean and saved it in src with all my other Lean files. At the top of my working file I have import relation_image.lean I'm getting an error.

[Andrew Lubrino]

I'm going to try the full file path and see if that works.

[Kevin Buzzard]

Look at my project; I don't use a full path (and it wouldn't work with a full path because / isn't in the search path for imports)

[Andrew Lubrino]

Yes, I should look at that.

[Andrew Lubrino]

I'll do that now

[Kevin Buzzard]

Saying "I'm getting an error" is really unhelpful. Even if you don't understand the error, you certainly aren't making anyone else's life easier by not saying what the error is. I guess you'd be better off posting a screenshot of your VS Code with the file explorer on the top left open.

[Andrew Lubrino]

got it. I didn't need the .lean file extension in the import. Thanks!

[Kevin Buzzard]

Oh yeah -- import data.set actually means import data.set.default so it was difficult to work out from your example :-)

[Andrew Lubrino]

I created a definition for the inverse image below. I've realized that there are a few things I'm confused about here:

-- the definition
def relation.image_inverse (A : set U) : set U := { x | ∃ y, x ∈ A ∧ R x y }

-- notation for the deiinition
notation R`⁻¹[[`:1024 A`]]`:1024 := relation.image_inverse R A

-- the API for the definition
lemma relation.image_inverse_def (A : set U) (x : U) : x ∈ R⁻¹[[A]] ↔ ∃ y, x ∈ A ∧ R x y :=
begin
  refl
end

I pretty much followed your example exactly for the notation. What does 1024 mean? I found somewhere that it has something to do with left binding or something, but I don't know what that means. Again for the notation, we set the notation equal to relation.image_inverse R A. I copied this pretty much exactly from your example again, but I can't figure out what the Ris doing in there. In the definition, there is only one argument, but it seems like here relation.image_inverse and the original relatino.image take two arguments. Is there any good documentation that explains this?

Thanks!

[Kevin Buzzard]

Your code doesn't compile but I'm assuming that one of the lines you omitted was variable (R : ...) which means " if the user ever mentions R in a definition or theorem statement, add R as an explicit input".

The 1024 is indeed binding power. Remove it and see what breaks. I wrote a blog post about it once

[Andrew Lubrino]

Okay, I understand. In this case, the definition was { y | ∃ x, x ∈ A ∧ R x y }, which includes R, so we needed it there as an input. I'm experimenting a bit here, below is the full code just for reference.

import data.set
open set

variable {U : Type}
variables A B: set U
variable R : U → U → Prop

-- the definition
def relation.image_inverse (A : set U) : set U := { x | ∃ y, x ∈ A ∧ R x y }

-- notation for the deiinition
notation R`⁻¹[[`:1024 A`]]`:1024 := relation.image_inverse R A

-- the API for the definition
lemma relation.image_inverse_def (A : set U) (x : U) : x ∈ R⁻¹[[A]] ↔ ∃ y, x ∈ A ∧ R x y :=
begin
  refl
end

I have variables A B: set U. My thought is that since I have variables A B: set U at the top, I shouldn't need to list A or B as arguments to any def or theorem (and perhaps also lemma) that uses those variables. I have (A : set U) as an argument to relation.image_inverse. When I remove (A : set U) from relation.image_inverse, I get an error at relation.image_inverse_def with the name type mismatch at application relation.image_inverse R. What's going wrong in this case? I'm not sure why A B : set U seems to be treated differently from R.

[Andrew Lubrino]

sorry part of my message was cut off, let me edit really quickly

[Andrew Lubrino]

Okay, the question is good to go now.