Require Export sets functions.
Section Image.
Variable A B : Type.
Definition direct_img(f : A → B)(P : set A) : set B :=
fun(b : B) ⇒ ∃(a : A), f a = b ∧ P a.
Definition inv_img(f : A → B)(P : set B) : set A :=
fun(a : A) ⇒ P (f a).
Lemma set_equal_inv_img :
∀(f g : A → B)(P Q : set B),
f ≡ g → set_equal P Q → set_equal (inv_img f P) (inv_img g Q).
Lemma set_equal_inv_img_pred : ∀(f : A → B)(P Q : set B),
set_equal P Q → set_equal (inv_img f P) (inv_img f Q).
Lemma set_equal_inv_img_feq : ∀(f g : A → B)(P : set B),
f ≡ g → set_equal (inv_img f P) (inv_img g P).
Lemma feq_direct_img :
∀(f g : A → B)(P Q : set A),
f ≡ g → set_equal P Q → set_equal (direct_img f P) (direct_img g Q).
Lemma fibred_set_inverse : ∀(f : A → B)(P : set B),
set_inverse (inv_img f P) = inv_img f (set_inverse P).
Lemma fibred_intersection : ∀(f : A → B)(P Q : set B),
intersection (inv_img f P) (inv_img f Q) =
inv_img f (intersection P Q).
End Image.
Implicit Arguments direct_img [A B].
Implicit Arguments inv_img [A B].
Lemma inv_img_id : ∀{A : Type}(P : set A),
inv_img id P = P.
Lemma inv_img_compose :
∀(A B C : Type)(f : A → B)(g : B → C)(P : set C),
inv_img f (inv_img g P) = inv_img (g ∘ f) P.
This following lemma is the core of the "elementary boolean algebra"
reasoning in Lemma 4.13 on page 23.
Actually, what is really needed there is the same result with
assumption
is_full_set (set_inverse (intersection
(set_inverse (inv_img pi_1 P))
(set_inverse (inv_img pi_2 Q))))
However, then this lemma is only valid in classical logic,
see classic_axiom_neg_disjunction_other_case in classic.v
I leave the classical reasoning to the uses of this lemma.
is_full_set (set_inverse (intersection
(set_inverse (inv_img pi_1 P))
(set_inverse (inv_img pi_2 Q))))
Lemma inv_proj_full :
∀(A B : Type)(pi_1 : A × B → A)(pi_2 : A × B → B)
(P : set A)(Q : set B)(b : B),
pi_1 ≡ (@fst A B) →
pi_2 ≡ (@snd A B) →
is_full_set (union (inv_img pi_1 P) (inv_img pi_2 Q)) →
not (Q b) →
is_full_set (inv_img pi_1 P).
Lemma direct_image_left_adjoint :
∀(A B : Type)(f : A → B)(P : set A)(Q : set B),
subset P (inv_img f Q) ↔ subset (direct_img f P) Q.
∀(A B : Type)(pi_1 : A × B → A)(pi_2 : A × B → B)
(P : set A)(Q : set B)(b : B),
pi_1 ≡ (@fst A B) →
pi_2 ≡ (@snd A B) →
is_full_set (union (inv_img pi_1 P) (inv_img pi_2 Q)) →
not (Q b) →
is_full_set (inv_img pi_1 P).
Lemma direct_image_left_adjoint :
∀(A B : Type)(f : A → B)(P : set A)(Q : set B),
subset P (inv_img f Q) ↔ subset (direct_img f P) Q.