Theory "quotient_pred_set"

Signature

Definitions

GSPECR_def

|- ∀R1 R2 f v. GSPECR R1 R2 f v ⇔ ∃x::respects R1. (R2 ### $<=>) (v,T) (f x)

SUBSETR_def

|- ∀R s t. SUBSETR R s t ⇔ ∀x::respects R. x ∈ s ⇒ x ∈ t

PSUBSETR_def

|- ∀R s t. PSUBSETR R s t ⇔ SUBSETR R s t ∧ ¬(R ===> $<=>) s t

INSERTR_def

|- ∀R x s. INSERTR R x s = {y | R y x ∨ y ∈ s}

DELETER_def

|- ∀R s x. DELETER R s x = {y | y ∈ s ∧ ¬R x y}

DISJOINTR_def

|- ∀R s t. DISJOINTR R s t ⇔ ¬∃x::respects R. x ∈ s ∧ x ∈ t

FINITER_def

|- ∀R s.
     FINITER R s ⇔
     ∀P::respects ((R ===> $<=>) ===> $<=>).
       P ∅ ∧
       (∀s::respects (R ===> $<=>). P s ⇒ ∀e::respects R. P (INSERTR R e s)) ⇒
       P s

IMAGER_def

|- ∀R1 R2 f s. IMAGER R1 R2 f s = {y | ∃x::respects R1. R2 y (f x) ∧ x ∈ s}

Theorems

IN_SET_MAP

|- ∀f s x. x ∈ (f --> I) s ⇔ f x ∈ s

SET_REL

|- ∀R s t. (R ===> $<=>) s t ⇔ ∀x y. R x y ⇒ (x ∈ s ⇔ y ∈ t)

SET_REL_MP

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀s t x y. (R ===> $<=>) s t ∧ R x y ⇒ (x ∈ s ⇔ y ∈ t)

IN_PRS

|- ∀R abs rep. QUOTIENT R abs rep ⇒ ∀x s. x ∈ s ⇔ rep x ∈ (abs --> I) s

IN_RSP

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀x1 x2 s1 s2. R x1 x2 ∧ (R ===> $<=>) s1 s2 ⇒ (x1 ∈ s1 ⇔ x2 ∈ s2)

IN_GSPECR

|- ∀R1 R2 f v. v ∈ GSPECR R1 R2 f ⇔ ∃x::respects R1. (R2 ### $<=>) (v,T) (f x)

GSPEC_PRS

|- ∀R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ⇒
     ∀R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ⇒
       ∀f. GSPEC f = (rep2 --> I) (GSPECR R1 R2 ((abs1 --> (rep2 ## I)) f))

GSPECR_RSP

|- ∀R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ⇒
     ∀R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ⇒
       ∀f1 f2.
         (R1 ===> R2 ### $<=>) f1 f2 ⇒
         (R2 ===> $<=>) (GSPECR R1 R2 f1) (GSPECR R1 R2 f2)

EMPTY_PRS

|- ∀R abs rep. QUOTIENT R abs rep ⇒ (∅ = (rep --> I) ∅)

EMPTY_RSP

|- ∀R abs rep. QUOTIENT R abs rep ⇒ (R ===> $<=>) ∅ ∅

UNIV_PRS

|- ∀R abs rep. QUOTIENT R abs rep ⇒ (𝕌(:β) = (rep --> I) 𝕌(:α))

UNIV_RSP

|- ∀R abs rep. QUOTIENT R abs rep ⇒ (R ===> $<=>) 𝕌(:α) 𝕌(:α)

UNION_PRS

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀s t. s ∪ t = (rep --> I) ((abs --> I) s ∪ (abs --> I) t)

UNION_RSP

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀s1 s2 t1 t2.
       (R ===> $<=>) s1 s2 ∧ (R ===> $<=>) t1 t2 ⇒
       (R ===> $<=>) (s1 ∪ t1) (s2 ∪ t2)

INTER_PRS

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀s t. s ∩ t = (rep --> I) ((abs --> I) s ∩ (abs --> I) t)

INTER_RSP

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀s1 s2 t1 t2.
       (R ===> $<=>) s1 s2 ∧ (R ===> $<=>) t1 t2 ⇒
       (R ===> $<=>) (s1 ∩ t1) (s2 ∩ t2)

SUBSET_PRS

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀s t. s ⊆ t ⇔ SUBSETR R ((abs --> I) s) ((abs --> I) t)

SUBSETR_RSP

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀s1 s2 t1 t2.
       (R ===> $<=>) s1 s2 ∧ (R ===> $<=>) t1 t2 ⇒
       (SUBSETR R s1 t1 ⇔ SUBSETR R s2 t2)

PSUBSET_PRS

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀s t. s ⊂ t ⇔ PSUBSETR R ((abs --> I) s) ((abs --> I) t)

PSUBSETR_RSP

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀s1 s2 t1 t2.
       (R ===> $<=>) s1 s2 ∧ (R ===> $<=>) t1 t2 ⇒
       (PSUBSETR R s1 t1 ⇔ PSUBSETR R s2 t2)

IN_INSERTR

|- ∀R x s y. y ∈ INSERTR R x s ⇔ R y x ∨ y ∈ s

INSERT_PRS

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀s x. x INSERT s = (rep --> I) (INSERTR R (rep x) ((abs --> I) s))

INSERTR_RSP

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀x1 x2 s1 s2.
       R x1 x2 ∧ (R ===> $<=>) s1 s2 ⇒
       (R ===> $<=>) (INSERTR R x1 s1) (INSERTR R x2 s2)

IN_DELETER

|- ∀R s x y. y ∈ DELETER R s x ⇔ y ∈ s ∧ ¬R x y

DELETE_PRS

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀s x. s DELETE x = (rep --> I) (DELETER R ((abs --> I) s) (rep x))

DELETER_RSP

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀s1 s2 x1 x2.
       (R ===> $<=>) s1 s2 ∧ R x1 x2 ⇒
       (R ===> $<=>) (DELETER R s1 x1) (DELETER R s2 x2)

DIFF_PRS

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀s t. s DIFF t = (rep --> I) ((abs --> I) s DIFF (abs --> I) t)

DIFF_RSP

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀s1 s2 t1 t2.
       (R ===> $<=>) s1 s2 ∧ (R ===> $<=>) t1 t2 ⇒
       (R ===> $<=>) (s1 DIFF t1) (s2 DIFF t2)

DISJOINT_PRS

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀s t. DISJOINT s t ⇔ DISJOINTR R ((abs --> I) s) ((abs --> I) t)

DISJOINTR_RSP

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀s1 s2 t1 t2.
       (R ===> $<=>) s1 s2 ∧ (R ===> $<=>) t1 t2 ⇒
       (DISJOINTR R s1 t1 ⇔ DISJOINTR R s2 t2)

FINITE_PRS

|- ∀R abs rep. QUOTIENT R abs rep ⇒ ∀s. FINITE s ⇔ FINITER R ((abs --> I) s)

FINITER_EQ

|- ∀R s1 s2. (R ===> $<=>) s1 s2 ⇒ (FINITER R s1 ⇔ FINITER R s2)

FINITER_RSP

|- ∀R abs rep.
     QUOTIENT R abs rep ⇒
     ∀s1 s2. (R ===> $<=>) s1 s2 ⇒ (FINITER R s1 ⇔ FINITER R s2)

FINITER_EMPTY

|- ∀R. FINITER R ∅

FINITER_INSERTR

|- ∀R (s::respects (R ===> $<=>)).
     FINITER R s ⇒ ∀x::respects R. FINITER R (INSERTR R x s)

ABSORPTIONR

|- ∀R (x::respects R) (s::respects (R ===> $<=>)).
     x ∈ s ⇔ (R ===> $<=>) (INSERTR R x s) s

FINITER_INDUCT

|- ∀R (P::respects ((R ===> $<=>) ===> $<=>)).
     P ∅ ∧
     (∀s::respects (R ===> $<=>).
        FINITER R s ∧ P s ⇒ ∀e::respects R. e ∉ s ⇒ P (INSERTR R e s)) ⇒
     ∀s::respects (R ===> $<=>). FINITER R s ⇒ P s

IN_IMAGER

|- ∀R1 R2 y f s. y ∈ IMAGER R1 R2 f s ⇔ ∃x::respects R1. R2 y (f x) ∧ x ∈ s

IMAGE_PRS

|- ∀R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ⇒
     ∀R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ⇒
       ∀f s.
         IMAGE f s =
         (rep2 --> I) (IMAGER R1 R2 ((abs1 --> rep2) f) ((abs1 --> I) s))

IMAGER_RSP

|- ∀R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ⇒
     ∀R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ⇒
       ∀f1 f2 s1 s2.
         (R1 ===> R2) f1 f2 ∧ (R1 ===> $<=>) s1 s2 ⇒
         (R2 ===> $<=>) (IMAGER R1 R2 f1 s1) (IMAGER R1 R2 f2 s2)