| Description: Define the class of
cosets by 𝑅: 𝑥 and 𝑦 are cosets by
𝑅 iff there exists a set 𝑢 such
that both 𝑢𝑅𝑥 and
𝑢𝑅𝑦 hold, i.e., both 𝑥 and
𝑦
are are elements of the 𝑅
-coset of 𝑢 (see dfcoss2 38681 and the comment of dfec2 8640). 𝑅 is
usually a relation.
This concept simplifies theorems relating partition and equivalence: the
left side of these theorems relate to 𝑅, the right side relate to
≀ 𝑅 (see e.g. pet 39143).
Without the definition of ≀ 𝑅 we
should have to relate the right side of these theorems to a composition
of a converse (cf. dfcoss3 38682) or to the range of a range Cartesian
product of classes (cf. dfcoss4 38683), which would make the theorems
complicated and confusing. Alternate definition is dfcoss2 38681.
Technically, we can define it via composition (dfcoss3 38682) or as the
range of a range Cartesian product (dfcoss4 38683), but neither of these
definitions reveal directly how the cosets by 𝑅 relate to each
other. We define functions (df-funsALTV 38944, df-funALTV 38945) and
disjoints (dfdisjs 38971, dfdisjs2 38972, df-disjALTV 38968, dfdisjALTV2 38977)
with the help of it as well. (Contributed by Peter Mazsa,
9-Jan-2018.) |
