Functions

\import Algebra.Group
\import Algebra.Meta
\import Arith.Real
\import Arith.Real.Field
\import Function.Meta
\import Logic
\import Meta
\import Operations
\import Order.Lattice
\import Order.LinearOrder
\import Order.PartialOrder
\import Paths.Meta
\import Topology.MetricSpace
\import Topology.NormedAbGroup
\import Topology.NormedAbGroup.Real
\import Topology.UniformSpace
\import Topology.UniformSpace.Product

\lemma norm-metric {X : PseudoNormedAbGroup} : MetricMap X RealNormed norm \cowith
  | func-dist => rewrite (norm-dist,norm-dist) $ join-univ norm_-left $ simplify norm_-right

\lemma dist-uniform-map {X : PseudoMetricSpace} : UniformMap (X ⨯ X) RealNormed (\lam s => dist s.1 s.2) \cowith
  | func-uniform Eu => \case dist-uniform.2 Eu \with {
    | inP (eps,eps>0,h) => inP (_, X.makeUniform (RealAbGroup.half>0 eps>0), _, X.makeUniform (RealAbGroup.half>0 eps>0), \lam {_} (inP (_, inP (x,idp), _, inP (x',idp), idp)) => \case h (dist x x') \with {
      | inP (W,EW,g) => inP (_, inP (W, EW, idp), \lam {(y,y')} (xy<eps/2,x'y'<eps/2) => g $ LinearOrder.<_join-univ
          (linarith (RealAbGroup.half+half, X.dist-triang {x} {y} {x'}, X.dist-triang {y} {y'} {x'}, X.dist-symm {x'} {y'}))
          (linarith (RealAbGroup.half+half, X.dist-triang {y} {x} {y'}, X.dist-triang {x} {x'} {y'}, X.dist-symm {x} {y})))
    })
  }

\lemma real-meet-uniform : UniformMap (RealNormed ⨯ RealNormed) RealNormed \lam s => s.1 ∧ s.2 \cowith
  | func-uniform Eu => \case dist-uniform.2 Eu \with {
    | inP (eps,eps>0,h) => inP (_, RealNormed.makeUniform eps>0, _, RealNormed.makeUniform eps>0, \lam {_} (inP (_, inP (x,idp), _, inP (x',idp), idp)) => \case h (x ∧ x') \with {
      | inP (W,EW,g) => inP (_, inP (W, EW, idp), \lam {(y,y')} (xy<eps,x'y'<eps) => g $ RealAbGroup.abs_-_<
          (unfold (-) $ rewrite (RealAbGroup.meet_negative, RealAbGroup.join_+-left) $ LinearOrder.<_join-univ
            (RealAbGroup.<=_+ meet-left <=-refl <∘r RealAbGroup.abs>=id <∘r xy<eps)
            (RealAbGroup.<=_+ meet-right <=-refl <∘r RealAbGroup.abs>=id <∘r x'y'<eps))
          (unfold (-) $ rewrite (RealAbGroup.meet_negative, RealAbGroup.join_+-left) $ LinearOrder.<_join-univ
            (RealAbGroup.<=_+ meet-left <=-refl <∘r RealAbGroup.abs>=_- <∘r xy<eps)
            (RealAbGroup.<=_+ meet-right <=-refl <∘r RealAbGroup.abs>=_- <∘r x'y'<eps)))
    })
  }

\lemma real-join-uniform : UniformMap (RealNormed ⨯ RealNormed) RealNormed \lam s => s.1 ∨ s.2 \cowith
  | func-uniform Eu => \case dist-uniform.2 Eu \with {
    | inP (eps,eps>0,h) => inP (_, RealNormed.makeUniform eps>0, _, RealNormed.makeUniform eps>0, \lam {_} (inP (_, inP (x,idp), _, inP (x',idp), idp)) => \case h (x ∨ x') \with {
      | inP (W,EW,g) => inP (_, inP (W, EW, idp), \lam {(y,y')} (xy<eps,x'y'<eps) => g $ RealAbGroup.abs_-_<
          (unfold (-) $ rewrite (RealAbGroup.join_negative, RealAbGroup.join_+-right) $ LinearOrder.<_join-univ
            (RealAbGroup.<=_+ <=-refl meet-left <∘r RealAbGroup.abs>=id <∘r xy<eps)
            (RealAbGroup.<=_+ <=-refl meet-right <∘r RealAbGroup.abs>=id <∘r x'y'<eps))
          (unfold (-) $ rewrite (RealAbGroup.join_negative, RealAbGroup.join_+-right) $ LinearOrder.<_join-univ
            (RealAbGroup.<=_+ <=-refl meet-left <∘r RealAbGroup.abs>=_- <∘r xy<eps)
            (RealAbGroup.<=_+ <=-refl meet-right <∘r RealAbGroup.abs>=_- <∘r x'y'<eps)))
    })
  }