共通部分の逆像

逆像のf^-1 を f^* と書く。

// SerND 共通部分の逆像

target

 f^*(C)∩f^*(D) = f^*(C∩D)

proof
 target

  f^*(C)∩f^*(D) ⊆ f^*(C∩D)

 proof

  assume

   x∈(f^*(C)∩f^*(D)) ---(ass)

  expand by (集合の共通部分)

   x∈f^*(C) ∧ x∈f^*(D)

  expand $.1, $.2 by (写像の逆像)

   f(x)∈C ∧ f(x)∈D

  contract by (集合の共通部分)

   f(x)∈(C∩D)

  contract by (集合の逆像)

   x∈f^*(C∩D)

  use assumption (ass)

   x∈(f^*(C)∩f^*(D)) ⇒ x∈f^*(C∩D)

  introduce universal

   ∀x.(x∈(f^*(C)∩f^*(D)) ⇒ x∈f^*(C∩D))

  contract by (集合の包含)

   f^*(C)∩f^*(D)) ⊆ f^*(C∩D)

 end proof

 then

  f^*(C)∩f^*(D)) ⊆ f^*(C∩D) ---(lemma1)
 target

  f^*(C∩D) ⊆ f^*(C)∩f^*(D)

 proof

  … 省略 …

 end proof

 then

  f^*(C∩D) ⊆ f^*(C)∩f^*(D)
 concat with (lemma1)

  f^*(C∩D) ⊆ f^*(C)∩f^*(D) ∧ f^*(C)∩f^*(D)) ⊆ f^*(C∩D)

 contract by (集合のイコール)

  f^*(C∩D) = f^*(C)∩f^*(D)
end proof

then

 f^*(C∩D) = f^*(C)∩f^*(D) ---(共通部分の逆像)