Theorem inf_eq_half_smul_add_sub_abs_sub'

Modification history

2025-08-27 16:04

Mathlib/Algebra/Order/Module/Basic.lean

chore(Algebra/Order): move `x ⊓ y = (⅟2 : α) • (x + y - |y - x|)` (#28900) …

Modified inf_eq_half_smul_add_sub_abs_sub'View on Github →

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 →