集合のド・モルガンの法則

// SerND 集合のド・モルガンの法則
target

 X＼(A∩B) = (X＼A)∪(X＼B)

proof
 target

  X＼(A∩B) ⊆ (X＼A)∪(X＼B)

 proof

  assume

   x∈X＼(A∩B) ---(ass)

  expand by (集合の差)

   x∈X ∧ ¬(x∈A∩B)

  expand $.2.1 by (集合の共通部分)

   x∈X ∧ ¬(x∈A ∧ x∈B)

  rewrite $.2 by (ド・モルガンの法則)

   x∈X ∧ (¬(x∈A) ∨ ¬(x∈B))

  rewrite by (論理の分配法則)

   (x∈X)∧¬(x∈A) ∨ (x∈X)∧¬(x∈B)

  contract $.1, $.2 by (集合の差)

   (x∈X＼A) ∨ (x∈X＼B)

  contract by (集合の合併)

   x∈(X＼A)∪(X＼B)

  use assumption (ass)

   x∈X＼(A∩B) ⇒ x∈(X＼A)∪(X＼B)

  contract by 集合の包含

   X＼(A∩B) ⊆ (X＼A)∪(X＼B)

 end proof

 then

  X＼(A∩B) ⊆ (X＼A)∪(X＼B) ---(lemma1)
 target

  (X＼A)∪(X＼B) ⊆ X＼(A∩B)

 proof

   … 省略 …

 end proof

 then

  (X＼A)∪(X＼B) ⊆ X＼(A∩B)
 concat with (lemma1)

  (X＼A)∪(X＼B) ⊆ X＼(A∩B) ∧ X＼(A∩B) ⊆ (X＼A)∪(X＼B)

 contract by (集合のイコール)

  (X＼A)∪(X＼B) = X＼(A∩B)
end proof

then

 X＼(A∩B) = (X＼A)∪(X＼B) ---(集合のド・モルガンの法則)