Stream: Is there code for X?

Topic: continuous_sup

Scott Morrison (Mar 16 2021 at 09:34):

import topology.algebra.ordered

example {β : Type} [partial_order β] [topological_space β] [order_topology β] [semilattice_sup β] :
continuous (λ (p : β × β), p.fst ⊔ p.snd) :=
begin
sorry
end


(This is actually true, right? :-)

Sebastien Gouezel (Mar 16 2021 at 09:46):

There is docs#continuous_max . Is that enough for what you want to do?

Yep! Thanks.

Kenny Lau (Mar 16 2021 at 10:17):

Let β = ([0,1] x {0,1})/{(0,0)=(0,1) and (1,0)=(1,1)} so it looks like a <> shape

Kenny Lau (Mar 16 2021 at 10:17):

let x be the point (0.5, 0)

Kenny Lau (Mar 16 2021 at 10:17):

and let y range through (t, 1), t -> 0

Kenny Lau (Mar 16 2021 at 10:18):

then x sup y goes from (1,1) suddenly to x

Kenny Lau (Mar 16 2021 at 10:18):

@Scott Morrison maybe this is a counter-example?

David Wärn (Mar 16 2021 at 10:44):

In other words, if you look at the four-element lattice {0, 1} x {0, 1}, it has two elements that are indistinguishable in the order topology. But sup distinguishes them, so can't be continuous

Kenny Lau (Mar 16 2021 at 10:51):

oh I didn't think I could discretize my situation, idk why

Scott Morrison (Mar 16 2021 at 10:57):

Thanks all. I guess I should have asked "what are the hypotheses I need to make sup continuous, and where's the theorem". Happily Sebastien worked this out. :-)

Scott Morrison (Mar 16 2021 at 10:57):

I'm actually working in \bbR, so don't really care about the exact hypotheses for now. :-)

Last updated: May 16 2021 at 05:21 UTC