mathlib

76ddb2bb - feat(analysis/normed_space/lattice_ordered_group): introduce normed lattice ordered groups (#9274)

feat(analysis/normed_space/lattice_ordered_group): introduce normed lattice ordered groups (#9274) Motivated by Banach Lattices, this PR introduces normed lattice ordered groups and proves that they are topological lattices. To support this `has_continuous_inf` and `has_continuous_sup` mixin classes are also defined. Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>