# Set Intersection is Self-Distributive/Families of Sets

## Theorem

Let $I$ be an indexing set.

Let $\family {A_\alpha}_{\alpha \mathop \in I}$ and $\family {B_\alpha}_{\alpha \mathop \in I}$ be indexed families of subsets of a set $S$.

Then:

$\ds \map {\bigcap_{\alpha \mathop \in I} } {A_\alpha \cap B_\alpha} = \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cap \paren {\bigcap_{\alpha \mathop \in I} B_\alpha}$

where $\ds \bigcap_{\alpha \mathop \in I} A_i$ denotes the intersection of $\family {A_\alpha}$.

## Proof

 $\ds x$ $\in$ $\ds \map {\bigcap_{\alpha \mathop \in I} } {A_\alpha \cap B_\alpha}$ $\ds \leadsto \ \$ $\ds \forall \alpha \in I: \,$ $\ds x$ $\in$ $\ds A_\alpha \cap B_\alpha$ Definition of Intersection of Family $\ds \leadsto \ \$ $\ds \forall \alpha \in I: \,$ $\ds x$ $\in$ $\ds A_\alpha$ Definition of Set Intersection $\, \ds \land \,$ $\ds x$ $\in$ $\ds B_\alpha$ $\ds \leadsto \ \$ $\ds x$ $\in$ $\ds \bigcap_{\alpha \mathop \in I} A_\alpha$ Definition of Intersection of Family $\, \ds \land \,$ $\ds x$ $\in$ $\ds \bigcap_{\alpha \mathop \in I} B_\alpha$ Definition of Intersection of Family $\ds \leadsto \ \$ $\ds x$ $\in$ $\ds \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cap \paren {\bigcap_{\alpha \mathop \in I} B_\alpha}$ Definition of Set Intersection

Thus by definition of subset:

$\ds \map {\bigcap_{\alpha \mathop \in I} } {A_\alpha \cap B_\alpha} \subseteq \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cap \paren {\bigcap_{\alpha \mathop \in I} B_\alpha}$

$\Box$

 $\ds x$ $\in$ $\ds \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cap \paren {\bigcap_{\alpha \mathop \in I} B_\alpha}$ $\ds \leadsto \ \$ $\ds x$ $\in$ $\ds \bigcap_{\alpha \mathop \in I} A_\alpha$ Definition of Set Intersection $\, \ds \land \,$ $\ds x$ $\in$ $\ds \bigcap_{\alpha \mathop \in I} B_\alpha$ $\ds \leadsto \ \$ $\ds \forall \alpha \in I: \,$ $\ds x$ $\in$ $\ds A_\alpha$ Definition of Intersection of Family $\, \ds \land \,$ $\ds x$ $\in$ $\ds B_\alpha$ $\ds \leadsto \ \$ $\ds \forall \alpha \in I: \,$ $\ds x$ $\in$ $\ds A_\alpha \cap B_\alpha$ Definition of Set Intersection $\ds \leadsto \ \$ $\ds x$ $\in$ $\ds \map {\bigcap_{\alpha \mathop \in I} } {A_\alpha \cap B_\alpha}$ Definition of Intersection of Family

Thus by definition of subset:

$\ds \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cap \paren {\bigcap_{\alpha \mathop \in I} B_\alpha} \subseteq \map {\bigcap_{\alpha \mathop \in I} } {A_\alpha \cap B_\alpha}$

$\Box$

By definition of set equality:

$\ds \map {\bigcap_{\alpha \mathop \in I} } {A_\alpha \cap B_\alpha} = \paren {\bigcap_{\alpha \mathop \in I} A_\alpha} \cap \paren {\bigcap_{\alpha \mathop \in I} B_\alpha}$

$\blacksquare$
{"ft_lang_label":"__label__en","ft_lang_prob":0.50713104,"math_prob":1.0000048,"size":3424,"snap":"2022-27-2022-33","text_gpt3_token_len":1262,"char_repetition_ratio":0.28070176,"word_repetition_ratio":0.5924453,"special_character_ratio":0.4147196,"punctuation_ratio":0.09581882,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":1.0000048,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2022-07-01T19:19:56Z\",\"WARC-Record-ID\":\"<urn:uuid:fe07a15e-e29a-49d2-86f4-bab0a3df68c3>\",\"Content-Length\":\"52150\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:1cfe75a9-5a6f-4fc6-8453-5ca8025795bc>\",\"WARC-Concurrent-To\":\"<urn:uuid:0535976e-3fc3-4945-a522-4c6709518149>\",\"WARC-IP-Address\":\"172.67.198.93\",\"WARC-Target-URI\":\"https://proofwiki.org/wiki/Set_Intersection_is_Self-Distributive_over_Family_of_Sets\",\"WARC-Payload-Digest\":\"sha1:VHZKCGIFOUODC3KKDRYILZQDQXNBUTZ7\",\"WARC-Block-Digest\":\"sha1:XXTOSOJWE3VVTTHHCSOZ2URPECX6YB6U\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2022/CC-MAIN-2022-27/CC-MAIN-2022-27_segments_1656103945490.54_warc_CC-MAIN-20220701185955-20220701215955-00313.warc.gz\"}"}