## 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.

0/0=0 btw

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 / lifts 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