Okay, thank you for the hint! I think, I want to exclude empty sets in the family with my definition of _iDisj_ . So we would have an equivalence only for this case.
$p ( ( -. (/) e. ran B ) -> ( _iDisj_ B <-> Disj_ x e. A B ) ) $= ? $. Am 15.12.2024 um 23:18 schrieb Mario Carneiro:
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] <mailto:metamath%[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/32d869ad-5fe9-4535-bb00-72dad9ec7792%40gmx.de.
