Zulip Chat Archive

Stream: Is there code for X?

Topic: continuous_sup


view this post on Zulip 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? :-)

view this post on Zulip Sebastien Gouezel (Mar 16 2021 at 09:46):

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

view this post on Zulip Scott Morrison (Mar 16 2021 at 09:49):

Yep! Thanks.

view this post on Zulip 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

view this post on Zulip Kenny Lau (Mar 16 2021 at 10:17):

let x be the point (0.5, 0)

view this post on Zulip Kenny Lau (Mar 16 2021 at 10:17):

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

view this post on Zulip Kenny Lau (Mar 16 2021 at 10:18):

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

view this post on Zulip Kenny Lau (Mar 16 2021 at 10:18):

@Scott Morrison maybe this is a counter-example?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Mar 16 2021 at 10:51):

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

view this post on Zulip 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. :-)

view this post on Zulip 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