   Jaskinie Podróże Nurki Grafika Mizar Teksty Kulinaria Lemkov Namiary Mapa RSS English   Spelunka Trybików Mizar Artykuły Boole'owskie właściwości zbiorów YAC Software    Wróć Mizar Eddie Artykuły Równoważność automatów deter ministycznych i epsilon niedeter ministycznych Etykietowane systemy tranzycji stanów Kwantyfikatory w wyrażeniach regularnych - co najmniej m wystąpień Systemy przepisywania słów Kwantyfikatory w wyrażeniach regularnych - od m do n wystąpień Języki formalne - konkatenacja i domknięcie Boole'owskie właściwości zbiorów Homomorfizmy i izomorfizmy grup; grupa ilorazowa Liczby całkowite Syntaktyka Mizara-MSE   Boole'owskie właściwości zbiorów Artykuł zawiera definicje zbioru pustego i aksjomaty (w sensie Mizara-MSE) opisujące należenie do zbiorów, zawieranie zbiorów, sumę, iloczyn i różnicę zbiorów. Następnie przeprowadzone są dowody kilkunastu faktów dotyczących wyżej wymienionych relacji i funkcji. Część twierdzeń zaczerpniętych została z . Ze względu na brak możliwości definiowania funkcji w Mizarze-MSE, wszystkie twierdzenia musiały być sformułowane i udowodnione jedynie za pomocą rachunku predykatów. Sekcje: Aksjomaty Podzbiory Suma zbiorów Iloczyn zbiorów Różnica zbiorów Bibliografia:  Library Committee: "Boolean Properties of Sets - Theorems", Mizar Mathematical Library, 2002. Pełny artykuł ``` ::::::::::::::::::::::::::::::::::::: :: Written by Michal Trybulec 2007 :: ::::::::::::::::::::::::::::::::::::: environ :: Everything is a set: sort set; :: A set is an element of another set: pred set in set; :: A set is a subset of another set: pred set subset_of set; :: A set is the union of two sets: pred set union_of set, set; :: A set is the intersection of two sets: pred set inter_of set, set; :: A set is the difference of two sets: pred set diff_of set, set; reserve x, y, z, A, B, C for set; :: The empty set is a set with no elements in it: given empty being set such that AxEmpty: not ex x st x in empty; :: Two sets are equal if exactly the same elements are in both sets: AxEquality: for A, B holds A = B iff for x holds x in A iff x in B; :: A set is a subset of another set :: if all its elements are also in the other set: AxSubset: for A, B holds A subset_of B iff for x st x in A holds x in B; :: A set is the union of two sets if each of its elements :: is in one of those two sets: AxUnion: for A, B, C holds A union_of B, C iff for x holds x in A iff x in B or x in C; :: A set is the intersection of two sets if each of its elements :: is in both of those two sets: AxInter: for A, B, C holds A inter_of B, C iff for x holds x in A iff x in B & x in C; :: A set is the difference of two sets if it includes :: only those elements of the first set that are not in the second set: AxDiff: for A, B, C holds A diff_of B, C iff for x holds x in A iff x in B & not x in C; begin ::::::::::::::::::::::::::::::::::::: :: Subsets :: ::::::::::::::::::::::::::::::::::::: :: The empty set is a subset of all sets. :: {} c= A; ThSubset10: for A holds empty subset_of A proof let A; now let x; assume x in empty; hence x in A by AxEmpty; end; hence thesis by AxSubset; end; :: A set is a subset of itself (reflexivity of the subset relation). :: A c= A; ThSubset20: for A holds A subset_of A proof let A; now let x; assume x in A; hence x in A; end; hence thesis by AxSubset; end; :: Another proof of A c= A - by contradiction. ThSubset20': for A holds A subset_of A proof let A; assume not A subset_of A; then ex x st x in A & not x in A by AxSubset; then consider x such that L: x in A & not x in A; thus contradiction by L; end; :: If B is a subset of A, and C is a subset of B, :: then C is a subset of A (transitivity of the subset relation). :: A c= B & B c= C implies A c= C; ThSubset30: for A, B, C st C subset_of B & B subset_of A holds C subset_of A proof let A, B, C; assume A: C subset_of B & B subset_of A; BA: for x st x in B holds x in A by A, AxSubset; CB: for x st x in C holds x in B by A, AxSubset; now let x; assume x in C; then x in B by CB, AxSubset; hence x in A by BA, AxSubset; end; hence thesis by AxSubset; end; :: If two sets are each other's subsets, then they are equal :: (antisymmetry of the subset relation). :: A c= B & B c= A iff A = B; ThSubset40: for A, B holds A subset_of B & B subset_of A iff A = B proof let A, B; thus A subset_of B & B subset_of A implies A = B proof assume A: A subset_of B & B subset_of A; BA: for x st x in B holds x in A by A, AxSubset; AB: for x st x in A holds x in B by A, AxSubset; now let x; thus x in A iff x in B by AB, BA; end; hence thesis by AxEquality; end; assume A = B; then A: for x holds x in A iff x in B by AxEquality; AB: now let x; thus x in A implies x in B by A; end; BA: now let x; thus x in B implies x in A by A; end; thus thesis by AB, BA, AxSubset; end; :: If a set is a subset of the empty set, it is itself empty. :: A c= {} implies A = {}; ThSubset50: for A st A subset_of empty holds A = empty proof let A; assume A: A subset_of empty; empty subset_of A by ThSubset10; hence thesis by A, ThSubset40; end; ::::::::::::::::::::::::::::::::::::: :: Union :: ::::::::::::::::::::::::::::::::::::: :: The union of a set with itself is the set itself. :: A \/ A = A; ThUnion10: for A holds A union_of A, A proof let A; now let x; thus x in A iff x in A or x in A; end; hence thesis by AxUnion; end; :: The order of the sets in the union is irrelevant :: (commutativity of the union function). :: A \/ B = B \/ A; ThUnion20: for A, B, C st C union_of A, B holds C union_of B, A proof let A, B, C; assume C union_of A, B; then A: for x holds x in C iff x in A or x in B by AxUnion; now let x; thus x in C iff x in B or x in A by A; end; hence thesis by AxUnion; end; :: The union of a set with its subset is the set itself. :: A c= B implies A \/ B = B; ThUnion30: for A, B st A subset_of B holds B union_of A, B proof let A, B; assume A subset_of B; then A: for x st x in A holds x in B by AxSubset; now let x; thus x in B iff x in A or x in B by A; end; hence thesis by AxUnion; end; :: The union of a set and the empty set is the set itself. :: {} \/ A = A; ThUnion40: for A holds A union_of empty, A proof let A; empty subset_of A by ThSubset10; hence thesis by ThUnion30; end; :: If the union of two sets is empty, then both sets are empty. :: {} = A \/ B implies A = {}; ThUnion50: for A, B st empty union_of A, B holds A = empty proof let A, B; assume empty union_of A, B; then A: for x holds x in empty iff x in A or x in B by AxUnion; now let x; assume x in A; hence x in empty by A; end; then B: A subset_of empty by AxSubset; empty subset_of A by ThSubset10; hence thesis by B, ThSubset40; end; :: Associativity of the union function. :: (A \/ B) \/ C = A \/ (B \/ C); ThUnion60: for A, B, C, AB, BC, D being set st AB union_of A, B & BC union_of B, C holds D union_of AB, C iff D union_of A, BC proof let A, B, C, AB, BC, D be set; assume A: AB union_of A, B & BC union_of B, C; AB: for x holds x in AB iff x in A or x in B by A, AxUnion; BC: for x holds x in BC iff x in B or x in C by A, AxUnion; thus D union_of AB, C implies D union_of A, BC proof assume D union_of AB, C; then DAB: for x holds x in D iff x in AB or x in C by AxUnion; now let x; x in D iff x in AB or x in C by DAB; then x in D iff x in A or x in B or x in C by AB; hence x in D iff x in A or x in BC by BC; end; hence thesis by AxUnion; end; assume D union_of A, BC; then DBC: for x holds x in D iff x in A or x in BC by AxUnion; now let x; x in D iff x in A or x in BC by DBC; then x in D iff x in A or x in B or x in C by BC; hence x in D iff x in AB or x in C by AB; end; hence thesis by AxUnion; end; :: A \/ B = A \/ (A \/ B): ThUnion70: for A, B, AB, AAB being set st AB union_of A, B & AAB union_of A, AB holds AB = AAB proof let A, B, AB, AAB be set; assume A: AB union_of A, B & AAB union_of A, AB; AB: for x holds x in AB iff x in A or x in B by A, AxUnion; AAB: for x holds x in AAB iff x in A or x in AB by A, AxUnion; for x holds x in AB iff x in AAB proof let x; thus x in AB implies x in AAB by AAB; assume x in AAB; then x in A or x in AB by AAB; hence thesis by AB; end; hence thesis by AxEquality; end; :: Both arguments of the union function are subsets of the result. :: A \/ B = C implies A c= C; ThUnion80: for A, B, C st C union_of A, B holds A subset_of C proof let A, B, C; assume C union_of A, B; then A: for x holds x in C iff x in A or x in B by AxUnion; now let x; assume x in A; hence x in C by A; end; hence thesis by AxSubset; end; :: The union of two subsets of a set is too a subset of this set. :: A c= C & B c= C implies A \/ B c= C; ThUnion90: for A, B, C, AB being set st AB union_of A, B & A subset_of C & B subset_of C holds AB subset_of C proof let A, B, C, AB be set; assume A: AB union_of A, B & A subset_of C & B subset_of C; AB: for x holds x in AB iff x in A or x in B by A, AxUnion; AC: for x st x in A holds x in C by A, AxSubset; BC: for x st x in B holds x in C by A, AxSubset; now let x; assume x in AB; then x in A or x in B by AB; hence x in C by AC, BC; end; hence thesis by AxSubset; end; ::::::::::::::::::::::::::::::::::::: :: Intersection :: ::::::::::::::::::::::::::::::::::::: :: The intersection of a set with itself is the set itself. :: A /\ A = A; ThInter10: for A holds A inter_of A, A proof let A; now let x; thus x in A iff x in A & x in A; end; hence thesis by AxInter; end; :: The order of the sets in the intersection is irrelevant :: (commutativity of the intersection function). :: A /\ B = B /\ A; ThInter20: for A, B, C st C inter_of A, B holds C inter_of B, A proof let A, B, C; assume C inter_of A, B; then A: for x holds x in C iff x in A & x in B by AxInter; now let x; thus x in C iff x in B & x in A by A; end; hence thesis by AxInter; end; :: The intersection of a set with its subset is the subset. :: A c= B implies A /\ B = A; ThInter30: for A, B st A subset_of B holds A inter_of A, B proof let A, B; assume A subset_of B; then A: for x st x in A holds x in B by AxSubset; now let x; thus x in A iff x in A & x in B by A; end; hence thesis by AxInter; end; :: The intersection of a set and the empty set is empty. :: {} /\ A = {}; ThInter40: for A holds empty inter_of empty, A proof let A; empty subset_of A by ThSubset10; hence thesis by ThInter30; end; :: Associativity of the intersection function. :: (A /\ B) /\ C = A /\ (B /\ C); ThInter60: for A, B, C, AB, BC, D being set st AB inter_of A, B & BC inter_of B, C holds D inter_of AB, C iff D inter_of A, BC proof let A, B, C, AB, BC, D be set; assume A: AB inter_of A, B & BC inter_of B, C; AB: for x holds x in AB iff x in A & x in B by A, AxInter; BC: for x holds x in BC iff x in B & x in C by A, AxInter; thus D inter_of AB, C implies D inter_of A, BC proof assume D inter_of AB, C; then DAB: for x holds x in D iff x in AB & x in C by AxInter; now let x; x in D iff x in AB & x in C by DAB; then x in D iff x in A & x in B & x in C by AB; hence x in D iff x in A & x in BC by BC; end; hence thesis by AxInter; end; assume D inter_of A, BC; then DBC: for x holds x in D iff x in A & x in BC by AxInter; now let x; x in D iff x in A & x in BC by DBC; then x in D iff x in A & x in B & x in C by BC; hence x in D iff x in AB & x in C by AB; end; hence thesis by AxInter; end; :: A /\ B = A /\ (A /\ B): ThInter70: for A, B, AB, AAB being set st AB inter_of A, B & AAB inter_of A, AB holds AB = AAB proof let A, B, AB, AAB be set; assume A: AB inter_of A, B & AAB inter_of A, AB; AB: for x holds x in AB iff x in A & x in B by A, AxInter; AAB: for x holds x in AAB iff x in A & x in AB by A, AxInter; for x holds x in AB iff x in AAB proof let x; thus x in AB implies x in AAB proof assume C: x in AB; then x in A & x in B by AB; hence thesis by C, AAB; end; assume x in AAB; then x in A & x in AB by AAB; hence thesis by AB; end; hence thesis by AxEquality; end; :: Both arguments of the intersection function are supersets of the result. :: A /\ B = C implies C c= A; ThInter80: for A, B, C st C inter_of A, B holds C subset_of A proof let A, B, C; assume C inter_of A, B; then A: for x holds x in C iff x in A & x in B by AxInter; now let x; assume x in C; hence x in A by A; end; hence thesis by AxSubset; end; :: The intersection of two supersets of a set is too a superset of this set. :: C c= A & C c= B implies C c= A /\ B; ThInter90: for A, B, C, AB being set st AB inter_of A, B & C subset_of A & C subset_of B holds C subset_of AB proof let A, B, C, AB be set; assume A: AB inter_of A, B & C subset_of A & C subset_of B; AB: for x holds x in AB iff x in A & x in B by A, AxInter; AC: for x st x in C holds x in A by A, AxSubset; BC: for x st x in C holds x in B by A, AxSubset; now let x; assume x in C; then x in A & x in B by AC, BC; hence x in AB by AB; end; hence thesis by AxSubset; end; :: Distributiveness of intersection over union: :: A /\ (B \/ C) = (A /\ B) \/ (A /\ C); for A, B, C, BuC, AiB, AiC, AiBuC, AuBiAuC being set st AiBuC inter_of A, BuC & BuC union_of B, C & AuBiAuC union_of AiB, AiC & AiB inter_of A, B & AiC inter_of A, C holds AiBuC = AuBiAuC proof let A, B, C, BuC, AiB, AiC, AiBuC, AiBuAiC be set such that A: AiBuC inter_of A, BuC & BuC union_of B, C & AiBuAiC union_of AiB, AiC & AiB inter_of A, B & AiC inter_of A, C; AiBuC: for x holds x in AiBuC iff x in A & x in BuC by A, AxInter; BuC: for x holds x in BuC iff x in B or x in C by A, AxUnion; AiBuAiC: for x holds x in AiBuAiC iff x in AiB or x in AiC by A, AxUnion; AiB: for x holds x in AiB iff x in A & x in B by A, AxInter; AiC: for x holds x in AiC iff x in A & x in C by A, AxInter; for x holds x in AiBuC iff x in AiBuAiC proof let x; thus x in AiBuC implies x in AiBuAiC proof assume x in AiBuC; then x in A & x in BuC by AiBuC; then x in A & (x in B or x in C) by BuC; then x in A & x in B or x in A & x in C; then x in AiB or x in A & x in C by AiB; then x in AiB or x in AiC by AiC; hence thesis by AiBuAiC; end; assume x in AiBuAiC; then x in AiB or x in AiC by AiBuAiC; then x in AiB or x in A & x in C by AiC; then x in A & x in B or x in A & x in C by AiB; then x in A & (x in B or x in C); then x in A & x in BuC by BuC; hence thesis by AiBuC; end; hence thesis by AxEquality; end; :: Distributiveness of union over intersection: :: A \/ (B /\ C) = (A \/ B) /\ (A \/ C); for A, B, C, BiC, AuB, AuC, AuBiC, AuBiAuC being set st AuBiC union_of A, BiC & BiC inter_of B, C & AuBiAuC inter_of AuB, AuC & AuB union_of A, B & AuC union_of A, C holds AuBiC = AuBiAuC proof let A, B, C, BiC, AuB, AuC, AuBiC, AuBiAuC be set such that A: AuBiC union_of A, BiC & BiC inter_of B, C & AuBiAuC inter_of AuB, AuC & AuB union_of A, B & AuC union_of A, C; AuBiC: for x holds x in AuBiC iff x in A or x in BiC by A, AxUnion; BiC: for x holds x in BiC iff x in B & x in C by A, AxInter; AuBiAuC: for x holds x in AuBiAuC iff x in AuB & x in AuC by A, AxInter; AuB: for x holds x in AuB iff x in A or x in B by A, AxUnion; AuC: for x holds x in AuC iff x in A or x in C by A, AxUnion; for x holds x in AuBiC iff x in AuBiAuC proof let x; thus x in AuBiC implies x in AuBiAuC proof assume x in AuBiC; then x in A or x in BiC by AuBiC; then x in A or (x in B & x in C) by BiC; then (x in A or x in B) & (x in A or x in C); then x in AuB & (x in A or x in C) by AuB; then x in AuB & x in AuC by AuC; hence thesis by AuBiAuC; end; assume x in AuBiAuC; then x in AuB & x in AuC by AuBiAuC; then x in AuB & (x in A or x in C) by AuC; then (x in A or x in B) & (x in A or x in C) by AuB; then x in A or (x in B & x in C); then x in A or x in BiC by BiC; hence thesis by AuBiC; end; hence thesis by AxEquality; end; ::::::::::::::::::::::::::::::::::::: :: Difference :: ::::::::::::::::::::::::::::::::::::: :: The difference of a set and its superset is an empty set: :: A c= B implies A \ B = {} ThDiff10: for A, B st A subset_of B holds empty diff_of A, B proof let A, B; assume A subset_of B; then A: for x st x in A holds x in B by AxSubset; now let x; thus x in empty iff x in A & not x in B proof thus x in empty implies x in A & not x in B proof assume x in empty; hence x in A & not x in B by AxEmpty; end; assume x in A & not x in B; hence x in empty by A; end; end; hence thesis by AxDiff; end; :: The difference of an empty set and a set is an empty set: :: {} \ A = {} ThDiff20: for A holds empty diff_of empty, A proof let A; empty subset_of A by ThSubset10; hence thesis by ThDiff10; end; :: If two sets have no common elements, their difference is equal to the first set: :: A /\ B = {} implies A = A \ B ThDiff30: for A, B st empty inter_of A, B holds A diff_of A, B proof let A, B; assume empty inter_of A, B; then A: for x holds x in empty iff x in A & x in B by AxInter; B: not ex x st x in A & x in B proof assume ex x st x in A & x in B; then consider x such that C: x in A & x in B; x in empty by A, C; hence contradiction by AxEmpty; end; now let x; thus x in A iff x in A & not x in B proof thus x in A implies x in A & not x in B proof assume x in A; hence x in A & not x in B by B; end; assume x in A & not x in B; hence x in A; end; end; hence thesis by AxDiff; end; :: The difference of a set and an empty set is the set itself: :: A = A \ {} ThDiff40: for A holds A diff_of A, empty proof let A; empty inter_of empty, A by ThInter40; then empty inter_of A, empty by ThInter20; hence thesis by ThDiff30; end; :: The difference of a set with that set is an empty set: :: A \ A = {} ThDiff50: for A holds empty diff_of A, A proof let A; A subset_of A by ThSubset20; hence thesis by ThDiff10; end; :: The difference of two sets is a subsets of the first set: :: A \ B c= A ThDiff60: for A, B, AmB being set st AmB diff_of A, B holds AmB subset_of A proof let A, B, AmB be set; assume AmB diff_of A, B; then A: for x holds x in AmB iff x in A & not x in B by AxDiff; now let x; assume x in AmB; hence x in A by A; end; hence thesis by AxSubset; end; :: The intersection of the difference of two sets with the second set is an empty set: :: (A \ B) /\ B = {} ThDiff70: for A, B, AmB being set st AmB diff_of A, B holds empty inter_of AmB, B proof let A, B, AmB be set; assume AmB diff_of A, B; then A: for x holds x in AmB iff x in A & not x in B by AxDiff; now let x; thus x in empty iff x in AmB & x in B proof thus x in empty implies x in AmB & x in B proof assume x in empty; hence x in AmB & x in B by AxEmpty; end; assume x in AmB & x in B; hence x in empty by A; end; end; hence thesis by AxInter; end; :: The difference of the difference of two sets and the second set :: is equal to the difference of these two sets: :: (A \ B) \ B = A \ B ThDiff80: for A, B, AmB being set st AmB diff_of A, B holds AmB diff_of AmB, B proof let A, B, AmB be set; assume AmB diff_of A, B; then A: for x holds x in AmB iff x in A & not x in B by AxDiff; now let x; thus x in AmB iff x in AmB & not x in B proof thus x in AmB implies x in AmB & not x in B proof assume x in AmB; hence thesis by A; end; assume x in AmB & not x in B; hence x in AmB; end; end; hence thesis by AxDiff; end;``` Góra