\import Algebra.Group
\import Algebra.Ordered
\import Function.Meta
\import Meta
\import Order.Directed
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Topology.TopAbGroup
\import Topology.TopSpace
\import Topology.TopSpace.Product
\open ProductTopSpace
\open ContMap

\class HausdorffTopPoset \extends HausdorffTopSpace, Poset {
  | <=-closed : (ProductTopSpace \this \this).IsClosed \lam s => s. <= s.
  | isHausdorff => \have P => ProductTopSpace \this \this \in
    hausdorff-char. $ transport P.IsClosed (ext \lam s => ext (\lam p => <=-antisymmetric p. p., \lam p => (=_<= p, =_<= (inv p)))) $ P.closed-inter <=-closed $ cont-closed (tuple proj2 proj1) <=-closed

  \lemma <=-closed-left {b : E} : IsClosed (`<= b)
    => cont-closed (tuple id (const b)) <=-closed

  \lemma <=-closed-right {a : E} : IsClosed (a <=)
    => cont-closed (tuple (const a) id) <=-closed

  \lemma limit-Join {I : DirectedSet} {f : I -> E} (fm : \Pi {i j : I} -> i I.<= j -> f i <= f j) {l : E} (fl : IsLimit f l) : IsJoin f l
    => (\lam i => closed-limit <=-closed-right fl fm, \lam u => closed-limit0 <=-closed-left fl u)

  \lemma limit-Meet {I : DirectedSet} {f : I -> E} (fm : \Pi {i j : I} -> i I.<= j -> f j <= f i) {l : E} (fl : IsLimit f l) : IsMeet f l
    => (\lam j => closed-limit <=-closed-left fl fm, \lam u => closed-limit0 <=-closed-right fl u)
}

\class HausdorffTopPosetAbGroup \extends HausdorffTopAbGroup, HausdorffTopPoset, PosetAbGroup {
  | positive-closed : IsClosed ( <=)

  \default <=-closed => transport (IsClosed {ProductTopSpace \this \this}) (ext \lam s => ext (from>=0,to>=0)) $ cont-closed (subtract-cont ContMap.∘ tuple proj2 proj1) positive-closed
  \default positive-closed => <=-closed-right
}