Non-expansiveness for big ops
A wish:
non-expansiveness for the big_op operations, e.g.
[∗ map] k ↦ x ∈ m, Φ k x
is non-expansive in m
, if m
is a gmap into an OFE
A wish:
non-expansiveness for the big_op operations, e.g.
[∗ map] k ↦ x ∈ m, Φ k x
is non-expansive in m
, if m
is a gmap into an OFE