documentation of `\;` needs fixing

[affeldt-aist]

analysis/classical/classical_sets.v

Line 209 in 7171aaf

(* A \; B == [set x | exists z, A (x.1, z) & B (z, x.2)] *)

Jean-Philippe Chancelier on Zulip on 2024-08-22:

there is also a little inconsistency between the comments at the begining of the file and the code
for relation composition. The composition of relation is described as
A \; B == [set x | exists z, A (x.1, z) & B (z, x.2)]
in the comments which is correct but implemented as
Notation "B \; A" := ([set xy | exists2 z, A (xy.1, z) & B (z, xy.2)]) : classical_set_scope.
"B \; A" should be "A \; B"