[Merged by Bors] - refactor(Topology/ContinuousFunction/Algebra): lattice ordered group gives inf/sup formula

[mans0954]

Previously the following comment occured in Topology.ContinuousFunction.Algebra:

-- TODO:
-- This lemma (and the next) could go all the way back in Algebra.Order.Field,
-- except that it is tedious to prove without tactics.
-- Rather than stranding it at some intermediate location,
-- it's here, immediately prior to the point of use.

Subsequently, the theory of lattice ordered groups has been developed in Mathlib (Algebra.Order.LatticeGroup). This now provides the natural "intermediate location" for these lemmas, they are an immediate consequence of LatticeOrderedCommGroup.two_inf_eq_add_sub_abs_sub and LatticeOrderedCommGroup.two_sup_eq_add_add_abs_sub. In fact we can show that C(α, β) is itself a lattice ordered group and hence expressions for the inf and sup (inf_eq and sup_eq) can be deduced directly from LatticeOrderedCommGroup.two_inf_eq_add_sub_abs_sub and LatticeOrderedCommGroup.two_sup_eq_add_add_abs_sub.

This was previously submitted to Mathlib leanprover-community/mathlib#18780

---

[eric-wieser]

LGTM

@semorrison, I think you might have written the inf_eq lemma; does this look good to you?

[j-loreaux]

This looks fine to me also. The inf_eq and sup_eq lemmas are easily obtained from the more general versions now, so I don't see any reason not to merge as is.

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style