no goals
α : Type u_1
inst✝⁴ : TopologicalSpace α
β : Type u_2
inst✝³ : LinearOrderedField β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : TopologicalRing β
f g : C(α, β)
x : α
⊢ ↑(f ⊓ g) x = ↑(2⁻¹ • (f + g - Abs.abs (f - g))) x
simpa using min_eq_half_add_sub_abs_sub