In lean 3, you can use (x y z OP e) as a binder whenever OP is a binary operation, and it abbreviates the binder sequence (x y z : _) (H : x OP e) (H : y OP e) (H : z OP e).

example : ∀ x < 5, x < 5 := λ x H, H

Lean 4 doesn't have a general mechanism for infix notations, so these have to be added individually for every combination of binding notation and operator (i.e. ∀ x < e, p x and ∃ x < e, p x and ∃ x ∈ S, p x all need to be defined separately). It is unclear what we even want to do here for translation purposes besides simple expansion.