Zulip Chat Archive

Stream: maths

Topic: Is every complete lattice compact?


view this post on Zulip Kenny Lau (Aug 23 2018 at 20:25):

Is every complete lattice compact? Here the topology is generated by sets of the form {x | a < x < b}

view this post on Zulip Kenny Lau (Aug 23 2018 at 20:33):

correction: the topology is generated by sets of the form {x | a < x < b} and {x | a < x} and {x | x < b}

view this post on Zulip Kevin Buzzard (Aug 23 2018 at 21:03):

I don't really understand the question but are the real numbers a counterexample?

view this post on Zulip Kenny Lau (Aug 23 2018 at 21:04):

it isn't a complete lattice

view this post on Zulip Johannes Hölzl (Aug 24 2018 at 07:14):

at least complete linear orders on a second countable topology form a complete lattice
compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)

view this post on Zulip Johannes Hölzl (Aug 24 2018 at 07:15):

In Isabelle the proof goes over:

lemma compact_complete_linorder:
  fixes X :: "nat ⇒ 'a::{complete_linorder,linorder_topology}"
  shows "∃l r. strict_mono r ∧ (X ∘ r) ⇢ l"

view this post on Zulip Johannes Hölzl (Aug 24 2018 at 07:16):

strict_mono means strictly increasing


Last updated: May 18 2021 at 07:19 UTC