--- /dev/null
+(** This module (Toolbox - subsets: operations) defines:
+ - subset binary intersection: [SAnd] (subset and)
+ - subset binary union: [SOr] (subset or)
+ - subset implication: [SImp] (subset implies)
+ - subset opposite: [SNot] (subset not)
+ - subset infinitary intersection: [SAll] (subset all)
+ - subset infinitary union: [SEx] (subset exists)
+
+ and provides:
+ - introduction and elimination rules for the defined constants
+ - standard properties (idempotency, commutativity, associativity, compatibility, distributivity) for the defined constants
+ - Cantor's diagonalization theorem: [cantor_diag]
+
+% \hrule %
+
+ We require Toolbox relations and the underlying theory.
+
+ *)
+Require Export tbs_rel.
+
+Section Subset_Operations_Definitions.
+
+ Section finitary_subset_operations.
+
+(** Subset and: [(SAnd S U V)] corresponds to $ U \sand_S V $. *)
+ Definition SAnd: (S:Set) (S -> Set) -> (S -> Set) -> (S -> Set).
+ Intros S U V a.
+ Exact (LAnd (U a) (V a)).
+ Defined.
+
+(** Subset or: [(SOr S U V)] corresponds to $ U \sor_S V $. *)
+ Definition SOr: (S:Set) (S -> Set) -> (S -> Set) -> (S -> Set).
+ Intros S U V a.
+ Exact (LOr (U a) (V a)).
+ Defined.
+
+(** Subset implies: [(SImp S U V)] corresponds to $ U \simp_S V $. *)
+ Definition SImp: (S:Set) (S -> Set) -> (S -> Set) -> (S -> Set).
+ Intros S U V a.
+ Exact (U a)->(V a).
+ Defined.
+
+(** Subset not: [(SNot S U)] corresponds to $ \snot_S U $. *)
+ Definition SNot: (S:Set) (S -> Set) -> (S -> Set).
+ Intros S U a.
+ Exact (LNot (U a)).
+ Defined.
+
+ End finitary_subset_operations.
+
+ Section infinitary_subset_operations.
+
+(** Subset all: [(SAll I S F)] corresponds to $ \bigsand_S\subset{F(i) \st i \in I} $. *)
+ Definition SAll: (I,S:Set) (I -> S -> Set) -> (S -> Set).
+ Intros I S F a.
+ Exact (i:I)(F i a).
+ Defined.
+
+(** Subset exists: [(SEx I S F)] corresponds to $ \bigsor_S\subset{F(i) \st i \in I} $. *)
+ Definition SEx: (I,S:Set) (I -> S -> Set) -> (S -> Set).
+ Intros I S F a.
+ Exact (LEx I [i](F i a)).
+ Defined.
+
+ End infinitary_subset_operations.
+
+End Subset_Operations_Definitions.
+
+Section Subset_Operations_Results.
+
+ Section subset_binary_intersection.
+
+(** Subset and, epsilon introduction: $ a \e U \limp a \e V \limp a \e U \sand V $. *)
+ Theorem sand_eps_i: (S:Set; U,V:S->Set; a:S) (Eps S a U) -> (Eps S a V) -> (Eps S a (SAnd S U V)).
+ Intros.
+ MApply 'eps_i.
+ Unfold SAnd.
+ MApply 'land_i.
+ MApply 'eps_e.
+ MApply 'eps_e.
+ Qed.
+
+(** Subset and, epsilon elimination 2: $ a \e U \sand V \limp a \e U $. *)
+ Theorem sand_eps_e2: (S:Set; V,U:S->Set; a:S) (Eps S a (SAnd S U V)) -> (Eps S a U).
+ Intros.
+ MApply 'eps_i.
+ MApply '(land_e2 (V a)).
+ Fold (SAnd S U V a).
+ MApply 'eps_e.
+ Qed.
+
+(** Subset and, epsilon elimination 1: $ a \e U \sand V \limp a \e V $. *)
+ Theorem sand_eps_e1: (S:Set; U,V:S->Set; a:S) (Eps S a (SAnd S U V)) -> (Eps S a V).
+ Intros.
+ MApply 'eps_i.
+ MApply '(land_e1 (U a)).
+ Fold (SAnd S U V a).
+ MApply 'eps_e.
+ Qed.
+
+(** Subset and, epsilon criterion: $ a \e U \land a \e V \liff a \e U \sand V $ *)
+ Theorem sand_eps: (S:Set; U,V:S->Set; a:S) (LIff (LAnd (Eps S a U) (Eps S a V)) (Eps S a (SAnd S U V))).
+ Intros.
+ MApply 'liff_i.
+ MApply 'sand_eps_i.
+ MApply '(land_e2 (Eps S a V)).
+ MApply '(land_e1 (Eps S a U)).
+ MApply 'land_i.
+ MApply '(sand_eps_e2 S V).
+ MApply '(sand_eps_e1 S U).
+ Qed.
+
+(** Subset and, sub or equal elimination 2: $ U \sand V \sub U $. *)
+ Theorem sand_sbe_e2: (S:Set; U,V:S->Set) (SbE S (SAnd S U V) U).
+ Intros.
+ MApply 'sbe_i.
+ MApply '(sand_eps_e2 S V).
+ Qed.
+
+(** Subset and, sub or equal elimination 1: $ U \sand V \sub V $. *)
+ Theorem sand_sbe_e1: (S:Set; U,V:S->Set) (SbE S (SAnd S U V) V).
+ Intros.
+ MApply 'sbe_i.
+ MApply '(sand_eps_e1 S U).
+ Qed.
+
+(** Subset and, sub or equal introduction: $ W \sub U \limp W \sub V \limp W \sub U \sand V $. *)
+ Theorem sand_sbe_i: (S:Set; W,U,V:S->Set) (SbE S W U) -> (SbE S W V) -> (SbE S W (SAnd S U V)).
+ Intros.
+ MApply 'sbe_i.
+ MApply 'sand_eps_i.
+ MApply '(sbe_e S W).
+ MApply '(sbe_e S W).
+ Qed.
+
+(** Subset and, sub or equal compatibility 2: $ U \sub V \limp U \sand W \sub V \sand W $. *)
+ Theorem sand_sbe_c2: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SAnd S U W) (SAnd S V W)).
+ Intros.
+ MApply 'sand_sbe_i.
+ MApply '(sbe_t S U).
+ MApply 'sand_sbe_e2.
+ MApply 'sand_sbe_e1.
+ Qed.
+
+(** Subset and, sub or equal subset top: $ U \sub \stop \sand U $. *)
+ Theorem sand_sbe_stop: (S:Set; U:S->Set) (SbE S U (SAnd S (STop S) U)).
+ Intros.
+ MApply 'sand_sbe_i.
+ MApply 'stop_sbe_i.
+ MApply 'sbe_r.
+ Qed.
+
+(** Subset and, sub or equal idempotency: $ U \sub U \sand U $. *)
+ Theorem sand_sbe_r: (S:Set; U:S->Set) (SbE S U (SAnd S U U)).
+ Intros.
+ MApply 'sand_sbe_i.
+ MApply 'sbe_r.
+ MApply 'sbe_r.
+ Qed.
+
+(** Subset and, idempotency $ U \sand U = U $. *)
+ Theorem sand_r: (S:Set; U:S->Set) (SEq S (SAnd S U U) U).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'sand_sbe_e2.
+ MApply 'sand_sbe_r.
+ Qed.
+
+(** Subset and, sub or equal commutativity: $ V \sand U \sub U \sand V $. *)
+ Theorem sand_sbe_s: (S:Set; U,V:S->Set) (SbE S (SAnd S V U) (SAnd S U V)).
+ Intros.
+ MApply 'sand_sbe_i.
+ MApply 'sand_sbe_e1.
+ MApply 'sand_sbe_e2.
+ Qed.
+
+(** Subset and, commutativity: $ V \sand U = U \sand V $. *)
+ Theorem sand_s: (S:Set; U,V:S->Set) (SEq S (SAnd S V U) (SAnd S U V)).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'sand_sbe_s.
+ MApply 'sand_sbe_s.
+ Qed.
+
+(** Subset and, sub or equal associativity 1: $ U \sand (V \sand W) \sub (U \sand V) \sand W $. *)
+ Theorem sand_sbe_a1: (S:Set; U,V,W:S->Set) (SbE S (SAnd S U (SAnd S V W)) (SAnd S (SAnd S U V) W)).
+ Intros.
+ MApply 'sand_sbe_i.
+ MApply 'sand_sbe_i.
+ MApply 'sand_sbe_e2.
+ MApply '(sbe_t S (SAnd S V W)).
+ MApply 'sand_sbe_e1.
+ MApply 'sand_sbe_e2.
+ MApply '(sbe_t S (SAnd S V W)).
+ MApply 'sand_sbe_e1.
+ MApply 'sand_sbe_e1.
+ Qed.
+
+(** Subset and, sub or equal associativity 2: $ (U \sand V) \sand W \sub U \sand (V \sand W) $. *)
+ Theorem sand_sbe_a2: (S:Set; U,V,W:S->Set) (SbE S (SAnd S (SAnd S U V) W) (SAnd S U (SAnd S V W))).
+ Intros.
+ MApply '(sbe_t S (SAnd S W (SAnd S U V))).
+ MApply 'sand_sbe_s.
+ MApply '(sbe_t S (SAnd S (SAnd S V W) U)).
+ MApply '(sbe_t S (SAnd S (SAnd S W U) V)).
+ MApply 'sand_sbe_a1.
+ MApply '(sbe_t S (SAnd S V (SAnd S W U))).
+ MApply 'sand_sbe_s.
+ MApply 'sand_sbe_a1.
+ MApply 'sand_sbe_s.
+ Qed.
+
+(** Subset and, associativity: $ U \sand (V \sand W) = (U \sand V) \sand W $. *)
+ Theorem sand_a: (S:Set; U,V,W:S->Set) (SEq S (SAnd S U (SAnd S V W)) (SAnd S (SAnd S U V) W)).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'sand_sbe_a1.
+ MApply 'sand_sbe_a2.
+ Qed.
+
+(** Subset and, sub or equal compatibility 1: $ U \sub V \limp W \sand U \sub W \sand V $. *)
+ Theorem sand_sbe_c1: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SAnd S W U) (SAnd S W V)).
+ Intros.
+ MApply '(sbe_t S (SAnd S U W)).
+ MApply 'sand_sbe_s.
+ MApply '(sbe_t S (SAnd S V W)).
+ MApply 'sand_sbe_c2.
+ MApply 'sand_sbe_s.
+ Qed.
+
+(** Subset and, sub or equal compatibility: $ U \sub V \limp W \sub X \limp U \sand W \sub V \sand X $. *)
+ Theorem sand_sbe_c: (S:Set; U,V,W,X:S->Set) (SbE S U V) -> (SbE S W X) -> (SbE S (SAnd S U W) (SAnd S V X)).
+ Intros.
+ MApply '(sbe_t S (SAnd S V W)).
+ MApply 'sand_sbe_c2.
+ MApply 'sand_sbe_c1.
+ Qed.
+
+ End subset_binary_intersection.
+
+ Section subset_binary_union.
+
+(** Subset or, epsilon introduction 2: $ a \e U \limp a \e U \sor V $. *)
+ Theorem sor_eps_i2: (S:Set; U,V:S->Set; a:S) (Eps S a U) -> (Eps S a (SOr S U V)).
+ Intros.
+ MApply 'eps_i.
+ Unfold SOr.
+ MApply 'in_l.
+ MApply 'eps_e.
+ Qed.
+
+(** Subset or, epsilon introduction 1: $ a \e V \limp a \e U \sor V $. *)
+ Theorem sor_eps_i1: (S:Set; U,V:S->Set; a:S) (Eps S a V) -> (Eps S a (SOr S U V)).
+ Intros.
+ MApply 'eps_i.
+ Unfold SOr.
+ MApply 'in_r.
+ MApply 'eps_e.
+ Qed.
+
+(** Subset or, epsilon elimination: $ (a \e U \limp T) \limp (a \e V \limp T) \limp a \e U \sor V \limp T $. *)
+ Theorem sor_eps_e: (S:Set; a:S; U,V:S->Set; T:Set) ((Eps S a U) -> T) -> ((Eps S a V) -> T) -> (Eps S a (SOr S U V)) -> T.
+ Intros.
+ MCut '(SOr S U V a).
+ MApply 'eps_e.
+ MApply '(lor_e (U a) (V a)).
+ MApply 'H.
+ MApply 'eps_i.
+ MApply 'H0.
+ MApply 'eps_i.
+ Qed.
+
+(** Subset or, epsilon criterion: $ a \e U \lor a \e V \liff a \e U \sor V $. *)
+ Theorem sor_eps: (S:Set; U,V:S->Set; a:S) (LIff (LOr (Eps S a U) (Eps S a V)) (Eps S a (SOr S U V))).
+ Intros.
+ MApply 'liff_i.
+ MApply '(lor_e (Eps S a U) (Eps S a V)).
+ MApply 'sor_eps_i2.
+ MApply 'sor_eps_i1.
+ MApply '(sor_eps_e S a U V).
+ MApply 'in_l.
+ MApply 'in_r.
+ Qed.
+
+(** Subset or, sub or equal introduction 2: $ U \sub U \sor V $. *)
+ Theorem sor_sbe_i2: (S:Set; U,V:S->Set) (SbE S U (SOr S U V)).
+ Intros.
+ MApply 'sbe_i.
+ MApply 'sor_eps_i2.
+ Qed.
+
+(** Subset or, sub or equal introduction 1: $ V \sub U \sor V $. *)
+ Theorem sor_sbe_i1: (S:Set; U,V:S->Set) (SbE S V (SOr S U V)).
+ Intros.
+ MApply 'sbe_i.
+ MApply 'sor_eps_i1.
+ Qed.
+
+(** Subset or, sub or equal elimination: $ U \sub W \limp V \sub W \limp U \sor V \sub W $. *)
+ Theorem sor_sbe_e: (S:Set; W,U,V:S->Set) (SbE S U W) -> (SbE S V W) -> (SbE S (SOr S U V) W).
+ Intros.
+ MApply 'sbe_i.
+ MApply '(sor_eps_e S a U V).
+ MApply '(sbe_e S U).
+ MApply '(sbe_e S V).
+ Qed.
+
+(** Subset or, sub or equal compatibility 2: $ U \sub V \limp U \sor W \sub V \sor W $. *)
+ Theorem sor_sbe_c2: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SOr S U W) (SOr S V W)).
+ Intros.
+ MApply 'sor_sbe_e.
+ MApply '(sbe_t S V).
+ MApply 'sor_sbe_i2.
+ MApply 'sor_sbe_i1.
+ Qed.
+
+(** Subset or, sub or equal idempotency: $ U \sor U \sub U $. *)
+ Theorem sor_sbe_r: (S:Set; U:S->Set) (SbE S (SOr S U U) U).
+ Intros.
+ MApply 'sor_sbe_e.
+ MApply 'sbe_r.
+ MApply 'sbe_r.
+ Qed.
+
+(** Subset or, idempotency: $ U \sor U = U $. *)
+ Theorem sor_r: (S:Set; U:S->Set) (SEq S (SOr S U U) U).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'sor_sbe_r.
+ MApply 'sor_sbe_i2.
+ Qed.
+
+(** Subset or, sub or equal commutativity: $ V \sor U \sub U \sor V $. *)
+ Theorem sor_sbe_s: (S:Set; U,V:S->Set) (SbE S (SOr S V U) (SOr S U V)).
+ Intros.
+ MApply 'sor_sbe_e.
+ MApply 'sor_sbe_i1.
+ MApply 'sor_sbe_i2.
+ Qed.
+
+(** Subset or, commutativity: $ V \sor U = U \sor V $. *)
+ Theorem sor_s: (S:Set; U,V:S->Set) (SEq S (SOr S V U) (SOr S U V)).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'sor_sbe_s.
+ MApply 'sor_sbe_s.
+ Qed.
+
+(** Subset or, sub or equal associativity 1: $ U \sor (V \sor W) \sub (U \sor V) \sor W $. *)
+ Theorem sor_sbe_a1: (S:Set; U,V,W:S->Set) (SbE S (SOr S U (SOr S V W)) (SOr S (SOr S U V) W)).
+ Intros.
+ MApply 'sor_sbe_e.
+ MApply '(sbe_t S (SOr S U V)).
+ MApply 'sor_sbe_i2.
+ MApply 'sor_sbe_i2.
+ MApply 'sor_sbe_e.
+ MApply '(sbe_t S (SOr S U V)).
+ MApply 'sor_sbe_i1.
+ MApply 'sor_sbe_i2.
+ MApply 'sor_sbe_i1.
+ Qed.
+
+(** Subset or, sub or equal associativity 2: $ (U \sor V) \sor W \sub U \sor (V \sor W) $. *)
+ Theorem sor_sbe_a2: (S:Set; U,V,W:S->Set) (SbE S (SOr S (SOr S U V) W) (SOr S U (SOr S V W))).
+ Intros.
+ MApply '(sbe_t S (SOr S W (SOr S U V))).
+ MApply 'sor_sbe_s.
+ MApply '(sbe_t S (SOr S (SOr S V W) U)).
+ MApply '(sbe_t S (SOr S (SOr S W U) V)).
+ MApply 'sor_sbe_a1.
+ MApply '(sbe_t S (SOr S V (SOr S W U))).
+ MApply 'sor_sbe_s.
+ MApply 'sor_sbe_a1.
+ MApply 'sor_sbe_s.
+ Qed.
+
+(** Subset or, associativity: $ U \sor (V \sor W) = (U \sor V) \sor W $. *)
+ Theorem sor_a: (S:Set; U,V,W:S->Set) (SEq S (SOr S U (SOr S V W)) (SOr S (SOr S U V) W)).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'sor_sbe_a1.
+ MApply 'sor_sbe_a2.
+ Qed.
+
+(** Subset or, sub or equal compatibility 1: $ U \sub V \limp W \sor U \sub W \sor V $. *)
+ Theorem sor_sbe_c1: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SOr S W U) (SOr S W V)).
+ Intros.
+ MApply '(sbe_t S (SOr S U W)).
+ MApply 'sor_sbe_s.
+ MApply '(sbe_t S (SOr S V W)).
+ MApply 'sor_sbe_c2.
+ MApply 'sor_sbe_s.
+ Qed.
+
+(** Subset or, sub or equal compatibility: $ U \sub V \limp W \sub X \limp U \sor W \sub V \sor X $. *)
+ Theorem sor_sbe_c: (S:Set; U,V,W,X:S->Set) (SbE S U V) -> (SbE S W X) -> (SbE S (SOr S U W) (SOr S V X)).
+ Intros.
+ MApply '(sbe_t S (SOr S V W)).
+ MApply 'sor_sbe_c2.
+ MApply 'sor_sbe_c1.
+ Qed.
+
+ End subset_binary_union.
+
+ Section subset_implication.
+
+(** Subset implies, epsilon introduction: $ (a \e U \limp a \e V) \limp a \e U \simp V $. *)
+ Theorem simp_eps_i: (S:Set; U,V:S->Set; a:S) ((Eps S a U) -> (Eps S a V)) -> (Eps S a (SImp S U V)).
+ Intros.
+ MApply 'eps_i.
+ Unfold SImp.
+ Intros.
+ MApply 'eps_e.
+ MApply 'H.
+ MApply 'eps_i.
+ Qed.
+
+(** Subset implies, epsilon elimination: $ a \e U \simp V \limp a \e U \limp a \e V $. *)
+ Theorem simp_eps_e: (S:Set; U,V:S->Set; a:S) (Eps S a (SImp S U V)) -> (Eps S a U) -> (Eps S a V).
+ Intros.
+ MApply 'eps_i.
+ Apply (mcut (U a)).
+ MApply 'eps_e.
+ MApply '(eps_e S a).
+ Qed.
+
+(** Subset implies, epsilon criterion: $ a \e U \simp V \liff (a \e U \limp a \e V) $. *)
+ Theorem simp_eps: (S:Set; U,V:S->Set; a:S) (LIff (Eps S a (SImp S U V)) (Eps S a U) -> (Eps S a V)).
+ Intros.
+ MApply 'liff_i.
+ MApply '(simp_eps_e S U).
+ MApply 'simp_eps_i.
+ MApply 'H.
+ Qed.
+
+(** Subset implies, sub or equal elimination: $ W \sub U \simp V \limp W \sand U \sub V $. *)
+ Theorem simp_sbe_e: (S:Set; U,V,W:S->Set) (SbE S W (SImp S U V)) -> (SbE S (SAnd S W U) V).
+ Intros.
+ MApply 'sbe_i.
+ MApply '(simp_eps_e S U).
+ MApply '(sbe_e S W).
+ MApply '(sand_eps_e2 S U).
+ MApply '(sand_eps_e1 S W).
+ Qed.
+
+(** Subset implies, sub or equal introduction: $ W \sand U \sub V \limp W \sub U \simp V $. *)
+ Theorem simp_sbe_i: (S:Set; U,V,W:S->Set) (SbE S (SAnd S W U) V) -> (SbE S W (SImp S U V)).
+ Intros.
+ MApply 'sbe_i.
+ MApply 'simp_eps_i.
+ MApply '(sbe_e S (SAnd S W U)).
+ MApply 'sand_eps_i.
+ Qed.
+
+(** Subset implies, sub or equal compatibility 2: $ V \sub U \limp U \simp W \sub V \simp W $. *)
+ Theorem simp_sbe_c2: (S:Set; U,V,W:S->Set) (SbE S V U) -> (SbE S (SImp S U W) (SImp S V W)).
+ Intros.
+ MApply 'simp_sbe_i.
+ MApply '(sbe_t S (SAnd S (SImp S U W) U)).
+ MApply 'sand_sbe_c1.
+ MApply 'simp_sbe_e.
+ MApply 'sbe_r.
+ Qed.
+
+(** Subset implies, sub or equal compatibility 2: $ U \sub V \limp W \simp U \sub W \simp V $. *)
+ Theorem simp_sbe_c1: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SImp S W U) (SImp S W V)).
+ Intros.
+ MApply 'simp_sbe_i.
+ MApply '(sbe_t S U).
+ MApply 'simp_sbe_e.
+ MApply 'sbe_r.
+ Qed.
+
+(** Subset implies, subset top elimination: $ \stop \sub U \simp V \limp U \sub V $. *)
+ Theorem simp_stop_e: (S:Set; U,V:S->Set) (SbE S (STop S) (SImp S U V)) -> (SbE S U V).
+ Intros.
+ MApply '(sbe_t S (SAnd S (STop S) U)).
+ MApply 'sand_sbe_stop.
+ MApply 'simp_sbe_e.
+ Qed.
+
+(** Subset implies, subset top introduction: $ U \sub V \limp \stop \sub U \simp V $. *)
+ Theorem simp_stop_i: (S:Set; U,V:S->Set) (SbE S U V) -> (SbE S (STop S) (SImp S U V)).
+ Intros.
+ MApply 'simp_sbe_i.
+ MApply '(sbe_t S U).
+ MApply 'sand_sbe_e1.
+ Qed.
+
+(** Subset implies, subset top criterion: $ \stop \sub U \simp V \liff U \sub V $. *)
+ Theorem simp_stop: (S:Set; U,V:S->Set) (LIff (SbE S (STop S) (SImp S U V)) (SbE S U V)).
+ Intros.
+ MApply 'liff_i.
+ MApply 'simp_stop_e.
+ MApply 'simp_stop_i.
+ Qed.
+
+ End subset_implication.
+
+ Section subset_negation.
+
+(** Subset not, epsilon introduction: $ \lnot (a \e U) \limp a \e \snot U $. *)
+ Theorem snot_eps_i: (S:Set; U:S->Set; a:S) (LNot (Eps S a U)) -> (Eps S a (SNot S U)).
+ Intros.
+ MApply 'eps_i.
+ Unfold SNot.
+ MApply 'lnot_i.
+ MApply '(lnot_e (Eps S a U)).
+ MApply 'eps_i.
+ Qed.
+
+(** Subset not, epsilon elimination: $ a \e \snot U \limp \lnot (a \e U) $. *)
+ Theorem snot_eps_e: (S:Set; U:S->Set; a:S) (Eps S a (SNot S U)) -> (LNot (Eps S a U)).
+ Unfold SNot.
+ Intros.
+ MApply 'lnot_i.
+ MApply '(lnot_e (U a)).
+ MApply '(eps_e S a [a0:S](LNot (U a0))).
+ MApply 'eps_e.
+ Qed.
+
+(** Subset not, epsilon criterion: $ \lnot (a \e U) \liff a \e \snot U $. *)
+ Theorem snot_eps: (S:Set; U:S->Set; a:S) (LIff (LNot (Eps S a U)) (Eps S a (SNot S U))).
+ Intros.
+ MApply 'liff_i.
+ MApply 'snot_eps_i.
+ MApply 'snot_eps_e.
+ Qed.
+
+(** Subset not, subset implication compatibility: $ \snot U = U \simp \sbot $. *)
+ Theorem snot_simp_c: (S:Set; U:S->Set) (SEq S (SNot S U) (SImp S U (SBot S))).
+ Intros.
+ MApply 'seq_i.
+ MApply 'simp_eps_i.
+ MCut 'Empty.
+ MApply '(lnot_e (Eps S a U)).
+ MApply 'snot_eps_e.
+ MElim 'H1 'efq.
+ MApply 'snot_eps_i.
+ MApply 'lnot_i.
+ MApply '(sbot_eps_e S a).
+ MApply '(simp_eps_e S U).
+ Qed.
+
+ End subset_negation.
+
+ Section subset_infinitary_intersection.
+
+(** Subset all, epsilon introduction: $ ((\lall i \in I)\ a \e F(i)) \limp a \e \bigsand\subset{F(i) \st i \in I} $. *)
+ Theorem sall_eps_i: (I,S:Set; F:(I->S->Set); a:S) ((i:I) (Eps S a (F i))) -> (Eps S a (SAll I S F)).
+ Intros.
+ MApply 'eps_i.
+ Unfold SAll.
+ Intros.
+ MApply 'eps_e.
+ MApply '(H i).
+ Qed.
+
+(** Subset all, epsilon elimination: $ a \e \bigsand\subset{F(i) \st i \in I} \limp (\lall i \in I)\ a \e F(i) $. *)
+ Theorem sall_eps_e: (I,S:Set; F:(I->S->Set); a:S) (Eps S a (SAll I S F)) -> (i:I) (Eps S a (F i)).
+ Intros.
+ MApply 'eps_i.
+ Apply (mcut (i:I)(F i a)).
+ MApply '(eps_e S a).
+ Intros.
+ MApply '(H0 i).
+ Qed.
+
+(** Subset all, epsilon criterion: $ a \e \bigsand\subset{F(i) \st i \in I} \liff (\lall i \in I)\ a \e F(i) $. *)
+ Theorem sall_eps: (I,S:Set; F:(I->S->Set); a:S) (LIff (Eps S a (SAll I S F)) (i:I) (Eps S a (F i))).
+ Intros.
+ MApply 'liff_i.
+ MApply '(sall_eps_e I).
+ MApply 'sall_eps_i.
+ MApply '(H i).
+ Qed.
+
+(** Subset all, sub or equal elimination: $ (\lall i \in I)\ \bigsand\subset{F(i) \st i \in I} \sub F(i) $. *)
+ Theorem sall_sbe_e: (I,S:Set; F:(I->S->Set); i:I) (SbE S (SAll I S F) (F i)).
+ Intros.
+ MApply 'sbe_i.
+ MApply '(sall_eps_e I).
+ Qed.
+
+(** Subset all, sub or equal introduction: $ ((\lall i \in I)\ W \sub F(i)) \limp W \sub \bigsand\subset{F(i) \st i \in I} $. *)
+ Theorem sall_sbe_i: (I,S:Set; F:(I->S->Set); W:S->Set) ((i:I)(SbE S W (F i))) -> (SbE S W (SAll I S F)).
+ Intros.
+ MApply 'sbe_i.
+ MApply 'sall_eps_i.
+ MApply '(sbe_e S W).
+ MApply 'H.
+ Qed.
+
+ End subset_infinitary_intersection.
+
+ Section subset_infinitary_union.
+
+(** Subset exists, epsilon introduction: $ ((\lex i \in I)\ a \e F(i)) \limp a \e \bigsor\subset{F(i) \st i \in I} $. *)
+ Theorem sex_eps_i: (I,S:Set; F:(I->S->Set); a:S) (LEx I [i](Eps S a (F i))) -> (Eps S a (SEx I S F)).
+ Intros.
+ MApply 'eps_i.
+ Unfold SEx.
+ MElim 'H 'lex_e.
+ MApply '(lex_i I a0).
+ MApply 'eps_e.
+ Qed.
+
+(** Subset exists, epsilon elimination: $ a \e \bigsor\subset{F(i) \st i \in I} \limp (\lex i \in I)\ a \e F(i) $. *)
+ Theorem sex_eps_e: (I,S:Set; F:(I->S->Set); a:S) (Eps S a (SEx I S F)) -> (LEx I [i](Eps S a (F i))).
+ Intros.
+ MCut '(SEx I S F a).
+ MApply 'eps_e.
+ MElim 'H0 'lex_e.
+ MApply '(lex_i I a0).
+ MApply 'eps_i.
+ Qed.
+
+(** Subset exists, epsilon elimination: $ a \e \bigsor\subset{F(i) \st i \in I} \liff (\lex i \in I)\ a \e F(i) $. *)
+ Theorem sex_eps: (I,S:Set; F:(I->S->Set); a:S) (LIff (Eps S a (SEx I S F)) (LEx I [i](Eps S a (F i)))).
+ Intros.
+ MApply 'liff_i.
+ MApply 'sex_eps_e.
+ MApply 'sex_eps_i.
+ Qed.
+
+(** Subset exists, sub or equal introduction: $ (\lall i \in I)\ F(i) \sub \bigsor\subset{F(i) \st i \in I} $. *)
+ Theorem sex_sbe_i: (I,S:Set; F:(I->S->Set); i:I) (SbE S (F i) (SEx I S F)).
+ Intros.
+ MApply 'sbe_i.
+ MApply 'sex_eps_i.
+ MApply '(lex_i I i).
+ Qed.
+
+(** Subset exists, sub or equal elimination: $ ((\lall i \in I)\ F(i) \sub W) \limp \bigsor\subset{F(i) \st i \in I} \sub W $. *)
+ Theorem sex_sbe_e: (I,S:Set; F:(I->S->Set); W:S->Set) ((i:I)(SbE S (F i) W)) -> (SbE S (SEx I S F) W).
+ Intros.
+ MApply 'sbe_i.
+ MCut '(LEx I [i:I](Eps S a (F i))).
+ MApply 'sex_eps_e.
+ MElim 'H1 'lex_e.
+ MApply '(sbe_e S (F a0)).
+ MApply 'H.
+ Qed.
+
+ End subset_infinitary_union.
+
+ Section subset_frame.
+
+(** Frame, subset and introduction: $ U \sub V \limp U \sand V = U $. *)
+ Theorem frame_sand_i: (S:Set; U,V:S->Set) (SbE S U V) -> (SEq S (SAnd S U V) U).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'sand_sbe_e2.
+ MApply '(sbe_t S (SAnd S U U)).
+ MApply 'sand_sbe_r.
+ MApply 'sand_sbe_c1.
+ Qed.
+
+(** Frame, subset and elimination: $ U \sand V = U \limp U \sub V $. *)
+ Theorem frame_sand_e: (S:Set; U,V:S->Set) (SEq S (SAnd S U V) U) -> (SbE S U V).
+ Intros.
+ MApply '(sbe_t S (SAnd S U V)).
+ MApply '(land_e1 (SbE S (SAnd S U V) U)).
+ MApply 'seq_sbe_e.
+ MApply 'sand_sbe_e1.
+ Qed.
+
+(** Frame, subset or introduction: $ U \sub V \limp U \sor V = V $. *)
+ Theorem frame_sor_i: (S:Set; U,V:S->Set) (SbE S U V) -> (SEq S (SOr S U V) V).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply '(sbe_t S (SOr S V V)).
+ MApply 'sor_sbe_c2.
+ MApply 'sor_sbe_r.
+ MApply 'sor_sbe_i1.
+ Qed.
+
+(** Frame, subset or elimination: $ U \sor V = V \limp U \sub V $. *)
+ Theorem frame_sor_e: (S:Set; U,V:S->Set) (SEq S (SOr S U V) V) -> (SbE S U V).
+ Intros.
+ MApply '(sbe_t S (SOr S U V)).
+ MApply 'sor_sbe_i2.
+ MApply '(land_e2 (SbE S V (SOr S U V))).
+ MApply 'seq_sbe_e.
+ Qed.
+
+(** Frame, subset exists introduction: $ \bigsor\subset{F(i) \st i \in I} \sand W \sub \bigsor\subset{F(i) \sand W \st i \in I} $. *)
+ Theorem frame_sex_i: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SAnd S (SEx I S F) W) (SEx I S [i](SAnd S (F i) W))).
+ Intros.
+ MApply 'sbe_i.
+ MApply 'sex_eps_i.
+ MCut '(Eps S a (SEx I S F)).
+ MApply '(sand_eps_e2 S W).
+ MCut '(LEx I [i:I](Eps S a (F i))).
+ MApply 'sex_eps_e.
+ MElim 'H1 'lex_e.
+ MApply '(lex_i I a0).
+ MApply 'sand_eps_i.
+ MApply '(sand_eps_e1 S (SEx I S F)).
+ Qed.
+
+(** Frame, subset exists elimination: $ \bigsor\subset{F(i) \sand W \st i \in I} \sub \bigsor\subset{F(i) \st i \in I} \sand W $. *)
+ Theorem frame_sex_e: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SEx I S [i]
+(SAnd S (F i) W)) (SAnd S (SEx I S F) W)).
+ Intros.
+ MApply 'sand_sbe_i.
+ MApply 'sex_sbe_e.
+ MApply '(sbe_t S (F i)).
+ MApply 'sand_sbe_e2.
+ MApply 'sex_sbe_i.
+ MApply 'sex_sbe_e.
+ MApply 'sand_sbe_e1.
+ Qed.
+
+(** Frame, subset exists distributivity: $ \bigsor\subset{F(i) \st i \in I} \sand W = \bigsor\subset{F(i) \sand W \st i \in I} $. *)
+ Theorem frame_sex_d: (I,S:Set; F:(I->S->Set); W:S->Set) (SEq S (SAnd S (SEx I S F) W) (SEx I S [i](SAnd S (F i) W))).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'frame_sex_i.
+ MApply 'frame_sex_e.
+ Qed.
+
+(** Frame, subset implies elimination: $ \bigsor\subset{F(i) \st i \in I} \simp W \sub \bigsand\subset{F(i) \simp W \st i \in I} $. *)
+ Theorem frame_simp_e: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SImp S (SEx I S F) W) (SAll I S [i](SImp S (F i) W))).
+ Intros.
+ MApply 'sall_sbe_i.
+ MApply 'simp_sbe_c2.
+ MApply 'sex_sbe_i.
+ Qed.
+
+(** Frame, subset implies introduction: $ \bigsand\subset{F(i) \simp W \st i \in I} \sub \bigsor\subset{F(i) \st i \in I} \simp W $. *)
+ Theorem frame_simp_i: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SAll I S [i](SImp S (F i) W)) (SImp S (SEx I S F) W)).
+ Intros.
+ MApply 'sbe_i.
+ MApply 'simp_eps_i.
+ MCut '(LEx I [i:I](Eps S a (F i))).
+ MApply 'sex_eps_e.
+ MElim 'H1 'lex_e.
+ MApply '(simp_eps_e S (F a0)).
+ MApply '(sall_eps_e I S [i:I](SImp S (F i) W)).
+ Qed.
+
+(** Frame, subset implies compatibility: $ \bigsor\subset{F(i) \st i \in I} \simp W = \bigsand\subset{F(i) \simp W \st i \in I} $. *)
+ Theorem frame_simp_c: (I,S:Set; F:(I->S->Set); W:S->Set) (SEq S (SImp S (SEx I S F) W) (SAll I S [i](SImp S (F i) W))).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'frame_simp_e.
+ MApply 'frame_simp_i.
+ Qed.
+
+ End subset_frame.
+
+ Section cantor_diagonalization.
+
+(** [(D S F)] is Cantor's subset $ D_F $. *)
+ Local D: (S:Set) (S -> S -> Set) -> (S -> Set).
+ Intros S F.
+ Exact (SNot S [a:S](F a a)).
+ Defined.
+
+(** Cantor's diagonalization: $ (\lall b \in S)\ \lnot (F(b) = D_F) $. *)
+ Theorem cantor_diag: (S:Set; F:S->S->Set) (b:S) (LNot (SEq S (F b) (D S F))).
+ Intros.
+ MApply 'lnot_i.
+ MCut '(LIff (Eps S b (F b)) (LNot (Eps S b (F b)))).
+ MApply 'liff_i.
+ MApply 'snot_eps_e.
+ Change (Eps S b (D S F)).
+ MApply '(seq_e1 S (F b)).
+ MApply '(seq_e2 S (D S F)).
+ Change (Eps S b (SNot S (F b))).
+ MApply 'snot_eps_i.
+ MApply '(lnot_liff_lbot (Eps S b (F b))).
+ Qed.
+
+ End cantor_diagonalization.
+
+End Subset_Operations_Results.
projects / helm.git / blobdiff