Commit 2023-08-01 19:57 11f20c48

refactor(Topology/ContinuousFunction/Algebra): lattice ordered group gives inf/sup formula (#6205) 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 https://github.com/leanprover-community/mathlib/pull/18780