Theorem inf_eq_half_smul_add_sub_abs_sub'

Modification history

2024-01-09 17:40
Mathlib/Algebra/Order/Group/PosPart.lean
chore: Move `x ⊔ y = (x + y + |y - x|) / 2` (#9466) …
Modified inf_eq_half_smul_add_sub_abs_sub'View on Github →
2023-08-01 19:57
Mathlib/Algebra/Order/LatticeGroup.lean
refactor(Topology/ContinuousFunction/Algebra): lattice ordered group gives inf/sup formula (#6205) …
Added inf_eq_half_smul_add_sub_abs_sub'View on Github →