Commit 2021-10-01 06:05 76ddb2bb
View on Github →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.