## Stream: maths

### Topic: extensions

#### Patrick Massot (Jul 16 2018 at 19:49):

@Johannes Hölzl At https://github.com/leanprover/mathlib/blob/master/analysis/topology/continuity.lean#L841-L843 do we really need that [inhabited γ]? It forces lots of other inhabited assumptions that seem unnecessary from a mathematical point of view. If γ is not inhabited then there shouldn't be that many f : α → γ to care about

#### Mario Carneiro (Jul 16 2018 at 19:55):

the inhabited is needed for lim

#### Mario Carneiro (Jul 16 2018 at 19:55):

because it takes a default value when the limit is not defined

#### Patrick Massot (Jul 16 2018 at 19:55):

I understand this

#### Patrick Massot (Jul 16 2018 at 19:55):

But one could hope for a definition not using lim then

#### Mario Carneiro (Jul 16 2018 at 19:57):

I recall puzzling over this definition a while ago; I also don't particularly like this style of definition

#### Mario Carneiro (Jul 16 2018 at 19:57):

it seems like we should already know that the limit is defined at this point

#### Mario Carneiro (Jul 16 2018 at 20:00):

I guess we need the assumption of continuous_ext to know the definition makes sense

#### Mario Carneiro (Jul 16 2018 at 20:02):

It forces lots of other inhabited assumptions that seem unnecessary from a mathematical point of view.

Do you have any particular examples?

#### Patrick Massot (Jul 16 2018 at 20:03):

Why? ext de is a function from α → γ to β → γ. Can't Lean be happy if both are uninhabited types and we don't write anything about the definition?

#### Patrick Massot (Jul 16 2018 at 20:04):

Examples are in my work in progress in the perfectoid project. I'm working on Hausdorff completions of uniform spaces.

#### Mario Carneiro (Jul 16 2018 at 20:04):

i mean maybe there is a way to pick an inhabitant in your setting

#### Patrick Massot (Jul 16 2018 at 20:04):

The completion functor, which is left-adjoint to the inclusion of Hausdorff and complete uniform spaces into all uniform spaces, is constructed on homs by extension

#### Patrick Massot (Jul 16 2018 at 20:05):

If I assume the starting uniform space is inhabited then its completion is also inhabited, no problem. But it mean I keep assuming spaces are inhabited

#### Mario Carneiro (Jul 16 2018 at 20:06):

No, I mean somehow argue the empty case so it's not needed

#### Patrick Massot (Jul 16 2018 at 20:07):

If this is possible there, why isn't possible right in the definition of dense_embedding.ext

#### Patrick Massot (Jul 16 2018 at 20:07):

(by the way, this name is confusion since it has nothing to do with extensionality)

#### Mario Carneiro (Jul 16 2018 at 20:08):

Agreed. Do you have a suggestion?

yes

#### Patrick Massot (Jul 16 2018 at 20:09):

dense_embedding.extension maybe?

#### Mario Carneiro (Jul 16 2018 at 20:19):

I managed this definition:

def extend (de : dense_embedding e) (f : α → γ) (b : β) : γ :=
have nonempty γ, from
let ⟨_, ⟨_, a, _⟩⟩ := exists_mem_of_ne_empty
(mem_closure_iff.1 (de.dense b) _ is_open_univ trivial) in ⟨f a⟩,
@lim _ (classical.inhabited_of_nonempty this) _ (map f (vmap e (nhds b)))


#### Patrick Massot (Jul 16 2018 at 20:20):

Scary! But I don't mind being scared by the definition: can you prove the expected properties?

#### Mario Carneiro (Jul 16 2018 at 20:20):

It's mostly just a proof getting stuck into the inhabited γ slot - it doesn't change any of the proofs

#### Mario Carneiro (Jul 16 2018 at 20:21):

all the proofs immediately after the definition still work, I may have to hunt down other uses

#### Patrick Massot (Jul 16 2018 at 20:26):

and also hunt down the inhabited assumptions

Last updated: May 14 2021 at 19:21 UTC