# Zulip Chat Archive

## Stream: new members

### Topic: Equality of function on intersection

#### Emiel Lanckriet (Aug 13 2020 at 14:02):

I tried to define a theorem where one of the conditions was an equality on an intersection, but I run into problems with types.

Here is a minimal example of the problem:

```
example {X Y : Type*} {A B : set X} (f : A → Y) (g: B → Y)
(h : ∀ (x ∈ A ∩ B), f x = g x) : Prop := true
```

Do I need to cast stuff or use coe in some form? How do I resolve this?

#### Kevin Buzzard (Aug 13 2020 at 14:07):

Your problem is that terms of type `set X`

are terms, not types, so you can't define functions on them without thinking a bit more carefully.

#### Kevin Buzzard (Aug 13 2020 at 14:09):

Given `A : set X`

there is a corresponding type, called a subtype of X. Lean will call it `\u A`

where `\u`

is some little up-arrow. But now you can see the problem -- if Lean uses subtypes then if x is in A \cap B, the set, then `x : X`

, so `f x`

doesn't make sense

#### Kevin Buzzard (Aug 13 2020 at 14:11):

```
import tactic
open set
example {X Y : Type*} {A B : set X} (f : A → Y) (g: B → Y)
(h : ∀ x : A ∩ B, f ⟨x.1, inter_subset_left _ _ x.2⟩ = g ⟨x.1, inter_subset_right _ _ x.2⟩) : Prop := true
```

#### Kevin Buzzard (Aug 13 2020 at 14:13):

`x : A ∩ B`

means that x is a term of type equal to the subtype corresponding to `A \cap B`

, so x is actually a pair: there's `x.1`

, which is a term of type `X`

, and there's `x.2`

, which is a proof that x is in A \cap B. We need to evaluate f on something-corresponding-to-x, but f only eats pairs <x,p> where p is a proof that x is in A, so you have to supply the proof that if x is in A \cap B then x is in A directly

#### Kevin Buzzard (Aug 13 2020 at 14:14):

If you think that this is a bit of a weird way to go about things, then you might want to consider the more normal type theory way to go about this stuff which would be to define f on all of X, and just let it be some junk value outside A. Then none of these problems occur.

#### Kevin Buzzard (Aug 13 2020 at 14:15):

This is why we have 0/0=1 in Lean -- it's just more convenient to let / be defined on all of a field k rather than just the subset of non-zero elements of k.

#### Kenny Lau (Aug 13 2020 at 14:16):

0/0=0 btw

#### Kevin Buzzard (Aug 13 2020 at 14:18):

0/0=junk value

#### Emiel Lanckriet (Aug 13 2020 at 14:38):

Okay, thanks, but I want to demand that f and g are continuous on their respective domains later (taking X and Y to be topological spaces), so how should I define these junk values in that case?

#### Kevin Buzzard (Aug 13 2020 at 14:55):

you can still say they're continuous on A and B by using filters. This is the technique used in mathlib. We say something about it in the perfectoid paper

#### Emiel Lanckriet (Aug 13 2020 at 15:21):

Okay, I'll look into it, thanks.

#### Eric Wieser (Aug 13 2020 at 15:46):

Would it be possible to allow

```
∀ x : A ∩ B, f ⟨x.1, inter_subset_left _ _ x.2⟩ = g ⟨x.1, inter_subset_right _ _ x.2⟩)
```

to be written

```
∀ x : A ∩ B, f (x : A) = g (x : B)
```

in @Kevin Buzzard's example? Do those `coe`

/ `lift`

s exist? If not, would it be sensible to add them?

#### Eric Wieser (Aug 13 2020 at 15:55):

This seems to work:

```
instance coe_left_inter {X : Type*} {A B : set X} : has_coe ↥(A ∩ B) ↥A := ⟨ λ x, ⟨x.1, inter_subset_left _ _ x.2⟩ ⟩
instance coe_right_inter {X : Type*} {A B : set X} : has_coe ↥(A ∩ B) ↥B := ⟨ λ x, ⟨x.1, inter_subset_right _ _ x.2⟩ ⟩
example {X Y : Type*} {A B : set X} (f : A → Y) (g: B → Y)
(h : ∀ x : A ∩ B, f x = g x) : Prop := true
```

#### Kevin Buzzard (Aug 13 2020 at 16:42):

did you try recompiling mathlib afterwards? Kind of looks dangerous...

#### Eric Wieser (Aug 13 2020 at 17:35):

No, I didn't. I assume using `has_lift`

instead of `has_coe`

would avoid any danger, but frankly I have no idea

#### Eric Wieser (Aug 13 2020 at 17:42):

Asked over at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Coercions.20on.20subtypes/near/206845831, since this isn't really a "new members" question any more.

Last updated: May 12 2021 at 05:19 UTC