# Zulip Chat Archive

## Stream: new members

### Topic: subtypes with equivalent properties

#### Jean Lo (Jun 06 2019 at 16:50):

This grew out of attempts at implementing things related to what was discussed in another thread, but I think it's generic enough that I should ask separately:

What is the (correct?) way of moving between subtypes of the same type defined by equivalent (but not definitionally equal)? For instance,

import data.real.basic -- i think these are different types. def f₁ : { x : ℝ // x < 1/2 } → ℝ := λ a, 1 def f₂ : { x : ℝ // 2 * x < 1 } → ℝ := λ a, 1 -- is there a non-awkward way of stating & invoking -- theorems like this? example : ∀ x, f₁ x = f₂ ⟨x.val, _⟩ := sorry

(context: if I glued two partial functions, I get a partial function (still of the same type! like `α →. β`

) whose domain is provably equal as a set to the union of the domains of the two functions I was gluing. Now I'm interested in having a statement for this gluing thing that instead takes two functions (say `f g : α → β`

) and two sets (`u v: set α`

), producing a function from `subtype (u ∪ v)`

— and now this seems like a tremendously bad idea, because if I do this sort of thing two or three times I wind up with a whole bunch of subtypes that all disagree with each other. Does there already exist a way of making this not-painful?)

#### Chris Hughes (Jun 06 2019 at 18:39):

`equiv.subtype_congr_prop`

. You can rewrite with the proof that the predicates are equal, but this `equiv`

gives better defeq

#### Jean Lo (Jun 06 2019 at 19:17):

Oh, how does this work in practice? I choose a subtype to state the theorem for, then I invoke `subtype_congr_prop`

every time I want to apply it to a term of another subtype with an equivalent prop?

#### Kevin Buzzard (Jun 06 2019 at 19:19):

Chris says yes -- choose one of them and always use that one

#### Jean Lo (Jun 06 2019 at 19:20):

great, thanks for the help!

#### Mario Carneiro (Jun 06 2019 at 19:20):

My inclination is to agree that this is a bad idea and you should stick with roption. You will actually get a bunch of subtypes of subtypes, and there are functions to deal with it, but it's not very convenient

#### Jean Lo (Jun 06 2019 at 19:36):

I agree that `roption`

is the right formulation for the stuff about gluing functions.

But at the same time I also want to write down things about partial functions from vector spaces and topologies and stuff, where the relevant lemmas in mathlib seem to usually be stated in terms of *'make a subtype out of a set (, the library code automatically puts the appropriate structure on it,) then work on that'.* For example, my interest in being able to do gluing began with wanting to construct piecewise functions with the pasting lemma (`continuous_subtype_is_closed_cover`

) , and currently to do that I seem to have to:

- define several partial functions, possibly by defining a (total) function, do
`pfun.lift`

, then`pfun.restrict`

it onto the domain I want. - glue them together.
- make the glued-together (partial) function a (total) function again
- use some sort of
`glue_eq`

lemma, together with`pfun.as_subtype`

, to put together the hypotheses`(f_cont : ∀i, continuous (λ(x : subtype (c i)), f x.val))`

before I can actually invoke the lemma. I guess it's to be expected that manipulating concrete examples like this is going to be tedious, but I still get the feeling that there's an amount of passing-back-and-forth-between-different-ways-of-writing-things that can possibly be avoided through some abstraction that I don't know yet.

#### Mario Carneiro (Jun 06 2019 at 19:54):

Isn't there a pasting lemma that uses `if`

?

#### Jean Lo (Jun 07 2019 at 05:54):

yeah, `continuous_if`

; it takes care of the case where the function is just defined piecewise as an `ite`

. But surely I'd still want to be able to do the same thing with any family of functions glued together (given a locally finite closed cover etc.) ?

#### Johannes Hölzl (Jun 07 2019 at 05:58):

Then use `continuous_subtype_is_closed_cover`

(Ah, now I see that you mentioned it already...)

#### Jean Lo (Jun 07 2019 at 06:03):

yeah. `continuous_subtype_is_closed_cover`

wants a total function together with proofs that its restrictions to functions from subtypes are continuous, and I was wondering whether there's a good way to feed it a bunch of functions from subtypes (or pfuns) and have it give me the continuity of the glued-together function that I wanted :D

#### Johannes Hölzl (Jun 07 2019 at 06:24):

Maybe you need to think it from the other side (which is obviously the same but sometimes makes a mental difference). You want to prove `continuous G`

(where `G`

is your glued-together function). Then you apply `continuous_subtype_is_closed_cover C`

, and get the statement that for each `c`

in `C`

you need to prove `continuous (fn x:subtype c, G (coe x))`

. But now you can rewrite `(fn x:subtype c, G (coe x))`

into something your like more.

#### Johannes Hölzl (Jun 07 2019 at 06:27):

The trick is that we now talk about `G (coe x)`

where `coe x`

gives us enough information to rewrite `G (coe x) = f_c (coe_2 x)`

where `c`

is the index into our cover, and `coe_2`

now may coerce from the cover into another set, the set where `f_c`

is defined on.

Last updated: May 09 2021 at 19:11 UTC