Stream: maths

Topic: Is every complete lattice compact?

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}

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}

Kevin Buzzard (Aug 23 2018 at 21:03):

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

Kenny Lau (Aug 23 2018 at 21:04):

it isn't a complete lattice

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)

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"


Johannes Hölzl (Aug 24 2018 at 07:16):

strict_mono means strictly increasing

Last updated: May 18 2021 at 07:19 UTC