continuous_sup

Stream: Is there code for X?

[Scott Morrison]

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]

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

[Scott Morrison]

Yep! Thanks.

[Kenny Lau]

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

[Kenny Lau]

let x be the point (0.5, 0)

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

@Scott Morrison maybe this is a counter-example?

[David Wärn]

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]

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

[Scott Morrison]

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]

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