Is every complete lattice compact?

Stream: maths

[Kenny Lau]

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

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kenny Lau]

it isn't a complete lattice

[Johannes Hölzl]

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]

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]

strict_mono means strictly increasing