Zulip Chat Archive

Stream: general

Topic: readable subquotients


view this post on Zulip Johan Commelin (Oct 01 2018 at 13:06):

So, let me return to my original question.

view this post on Zulip Johan Commelin (Oct 01 2018 at 13:07):

I've got

definition Spa (A : Huber_pair) : set (Spv A) :=
Spv.lift (λ v, v.is_continuous   r, r  A  v.val.val r  1)
(λ v₁ v₂ heq, sorry)

-- fake
definition Spa' (A : Huber_pair) : set (Spv A) :=
{v : Spv A | v.is_continuous   r, r  A  v.val.val r  1}
which_is_well_defined (λ v₁ v₂ heq, sorry)

view this post on Zulip Johan Commelin (Oct 01 2018 at 13:08):

Maybe it is really minor to people who have seen Lean for 367 days in the last year, but I think Spa' is a lot more readable than Spa.

view this post on Zulip Johan Commelin (Oct 01 2018 at 13:09):

Of course any mathematician who takes a first look is already brain-blocked by set (Spv A), which means "subset" instead of "set". But never mind...

view this post on Zulip Kevin Buzzard (Oct 01 2018 at 14:42):

Can't you put the work into the definition of v.is_continuous?

view this post on Zulip Johan Commelin (Oct 01 2018 at 14:44):

I'm not sure if that would help. Or do you mean that you want to define Spa as intersection of two subsets? Namely Cont and the other condition.

view this post on Zulip Johan Commelin (Oct 01 2018 at 14:45):

Still feels like moving the problem around...


Last updated: May 08 2021 at 10:12 UTC