That doesn't match the other of the two examples I gave: the family x e. A |-> (/) is always a disjoint family. This is not injective as a function because (/) is returned many times.
On Sun, Dec 15, 2024 at 4:57 PM Peter Dolland <[email protected]> wrote: > However, I would prefer to define the disjointness of an *indexed family* > by ensuring the injectivness of the index map: > > _iDisj_ iMap <-> ( Fun `' iMap /\ _disj_ ran iMap ) > > What do you think about? > Am 14.12.2024 um 23:09 schrieb Peter Dolland: > > Okay, thank you, I see the difference. > Am 14.12.2024 um 21:04 schrieb Mario Carneiro: > > `Disj_ x e. A B` is about disjointness of an *indexed family* of sets > B(x), where x ranges over the index set A. It says that if B(x) and B(y) > share a common element, then x = y. This is a stronger notion than > disjointness of a set of sets, which is what your _disj_ does, since here > you can conclude only that if B(x) and B(y) share a common element then > B(x) = B(y). For example, a family of empty sets of any cardinality is a > disjoint family, and a family of sets x e. A |-> { 0 } is disjoint if and > only if A has at most one element. You cannot express the latter theorem > using _disj_, because if you try to convert the indexed family into a set > of sets you just get { { 0 } } (or (/) if A is empty) which is a disjoint > family of sets. > > Conversely, you can define _disj_ in terms of Disj_ though: _disj_ A <-> > Disj x e. A x . > > On Sat, Dec 14, 2024 at 8:57 PM 'Peter Dolland' via Metamath < > [email protected]> wrote: > >> Can anybody help me to understand the definition of Disjointness: >> >> df-disj $a |- ( Disj_ x e. A B <-> A. y E* x e. A y e. B ) $. >> >> ? What means x, A, and B here? >> >> What about my alternative definition as 1-ary predicate: >> >> _disj_ A <-> A. B e. A A. C e. A ( B = C \/ B i^i C = (/) ) >> >> ? Would it be provable: >> >> $p _disj_ A <-> Disj_ x e. A B $= ? $. >> >> ? >> >> Thank you for your help! >> >> -- >> You received this message because you are subscribed to the Google Groups >> "Metamath" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To view this discussion visit >> https://groups.google.com/d/msgid/metamath/63763d29-b77a-4586-8664-74882baeaca6%40gmx.de >> . >> > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion visit > https://groups.google.com/d/msgid/metamath/CAFXXJStPS%3D0DJ4vh7LfkhzD1V4NSUG3W8%3DXJe6q8Osdmc2_6WQ%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAFXXJStPS%3D0DJ4vh7LfkhzD1V4NSUG3W8%3DXJe6q8Osdmc2_6WQ%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/CAFXXJSsTyaKa%3DRYsUT_jtoGyXPQr_4z_dC2%3DUifc_JMmLbbmmA%40mail.gmail.com.
