Theory: simpleSetCat

Type operators

(none)

Constants

Delta : (α -> bool) -> α -> α -> bool
Gr : (α -> β) -> (α -> bool) -> α -> β -> bool
RIMAGE : (α -> β) -> (α -> bool) -> (α -> α -> bool) -> β -> β -> bool
RINV_IMAGE : (α -> β) -> (α -> bool) -> (β -> β -> bool) -> α -> α -> bool
SPO : (γ -> bool) -> (α -> bool) -> (β -> bool) -> (γ -> α) -> (γ -> β) -> ((α + β -> bool) -> bool) # (α -> α + β -> bool) # (β -> α + β -> bool)
SPO_pimg : (α -> bool) -> (α -> β) -> (α -> γ) -> β + γ -> α -> bool
SPOr : (γ -> bool) -> (γ -> α) -> (γ -> β) -> α + β -> α + β -> bool
Spushout : (α -> bool) -> (β -> bool) -> (γ -> bool) -> (α -> β) -> (α -> γ) -> (π -> bool) # (β -> π) # (γ -> π) -> δ itself -> bool
cardgt : α itself -> num -> bool
eps : (α -> α -> bool) -> (α -> bool) -> α -> α -> bool
kernel : (α -> bool) -> (α -> β) -> α -> α -> bool
restr : (α -> β) -> (α -> bool) -> α -> β
shom : (α -> β) -> (α -> bool) -> (β -> bool) -> bool
span : (α -> bool) -> (α -> β) -> (α -> γ) -> β -> γ -> bool

Definitions

Delta_def Gr_def RIMAGE_def RINV_IMAGE_def SPO_def SPO_pimg_def SPOr_def cardgt_def eps_def kernel_def restr_def shom_def span_def

Theorems

Definitions

Delta_def

⊢ ∀V a b. Δ V a b ⇔ a = b ∧ a ∈ V

Gr_def

⊢ ∀h A a b. Gr h A a b ⇔ a ∈ A ∧ b = h a

RIMAGE_def

⊢ ∀f A R x y.
    RIMAGE f A R x y ⇔
    ∃x0 y0. x = f x0 ∧ y = f y0 ∧ R x0 y0 ∧ x0 ∈ A ∧ y0 ∈ A

RINV_IMAGE_def

⊢ ∀f A R x y. RINV_IMAGE f A R x y ⇔ x ∈ A ∧ y ∈ A ∧ R (f x) (f y)

SPO_def

⊢ ∀A B C f g.
    SPO A B C f g =
    (partition (SPOr A f g) (B ⊔ C),
     restr (λb. equiv_class (SPOr A f g) (B ⊔ C) (INL b)) B,
     restr (λc. equiv_class (SPOr A f g) (B ⊔ C) (INR c)) C)

SPO_pimg_def

⊢ (∀A f g x. SPO_pimg A f g (INL x) = PREIMAGE f {x} ∩ A) ∧
  ∀A f g y. SPO_pimg A f g (INR y) = PREIMAGE g {y} ∩ A

SPOr_def

⊢ ∀A f g.
    SPOr A f g =
    (λx y. (∃a. a ∈ A ∧ x = INL (f a) ∧ y = INR (g a)) ∨ x = y)^=

cardgt_def

⊢ ∀n. cardgt (:α) n ⇔ FINITE 𝕌(:α) ⇒ n < CARD 𝕌(:α)

eps_def

⊢ ∀R A a. eps R A a = if a ∈ A then {b | R a b ∧ b ∈ A} else ARB

kernel_def

⊢ ∀A f x y. kernel A f x y ⇔ x ∈ A ∧ y ∈ A ∧ f x = f y

restr_def

⊢ ∀f s. restr f s = (λx. if x ∈ s then f x else ARB)

shom_def

⊢ ∀f A B. shom f A B ⇔ (∀a. a ∈ A ⇒ f a ∈ B) ∧ ∀a. a ∉ A ⇒ f a = ARB

span_def

⊢ ∀A f g b d. span A f g b d ⇔ ∃a. a ∈ A ∧ b = f a ∧ d = g a

Theorems

Delta_IMAGE

⊢ Δ (IMAGE f A) = RIMAGE f A (Δ A)

Delta_INTER

⊢ Δ (s ∩ t) = Δ s ∩ᵣ Δ t

Gr_Id

⊢ Gr (λx. x) A = Δ A

Gr_restr

⊢ Gr (restr f A) A = Gr f A

IN_UNCURRY

⊢ (a,b) ∈ UNCURRY R ⇔ R a b

RIMAGE_Gr

⊢ RIMAGE f A R = Gr f A ∘ᵣ R ∘ᵣ (Gr f A)ᵀ

RINV_IMAGE_Gr

⊢ RINV_IMAGE f A R = (Gr f A)ᵀ ∘ᵣ R ∘ᵣ Gr f A

SPOr_REFL

⊢ SPOr A f g x x

SPOr_lemma

⊢ restr (j1 ∘ f) A = restr (j2 ∘ g) A ⇒
  (∀b1 b2. SPOr A f g (INL b1) (INL b2) ⇒ j1 b1 = j1 b2) ∧
  (∀b c. SPOr A f g (INL b) (INR c) ⇒ j1 b = j2 c) ∧
  (∀b' c'. SPOr A f g (INR c') (INL b') ⇒ j1 b' = j2 c') ∧
  ∀c1 c2. SPOr A f g (INR c1) (INR c2) ⇒ j2 c1 = j2 c2

Spushout_def

⊢ Spushout A B C' f g (P,i1,i2) (:δ) ⇔
  shom f A B ∧ shom g A C' ∧ shom i1 B P ∧ shom i2 C' P ∧
  restr (i1 ∘ f) A = restr (i2 ∘ g) A ∧
  ∀Q j1 j2.
    shom j1 B Q ∧ shom j2 C' Q ∧ restr (j1 ∘ f) A = restr (j2 ∘ g) A ⇒
    ∃!u. shom u P Q ∧ restr (u ∘ i1) B = j1 ∧ restr (u ∘ i2) C' = j2

Spushout_ind

⊢ ∀P'.
    (∀A B C f g P i1 i2. P' A B C f g (P,i1,i2) (:δ)) ⇒
    ∀v v1 v2 v3 v4 v5 v6 v7 v8. P' v v1 v2 v3 v4 (v5,v6,v7) v8

Spushout_quotient

⊢ shom f A B ∧ shom g A C ⇒ Spushout A B C f g (SPO A B C f g) (:δ)

Spushout_sym

⊢ Spushout A B C f g (P,p1,p2) (:δ) ⇒ Spushout A C B g f (P,p2,p1) (:δ)

Spushout_transfer

⊢ Spushout A B C f g (P,i1,i2) (:δ) ∧ INJ h 𝕌(:ε) 𝕌(:δ) ⇒
  Spushout A B C f g (P,i1,i2) (:ε)

Spushouts_iso

⊢ Spushout A B C f g (P,i1,i2) (:ε) ∧ Spushout A B C f g (Q,j1,j2) (:δ) ∧
  cardgt (:δ) 1 ∧ cardgt (:ε) 1 ⇒
  ∃H. BIJ H P Q ∧ restr (H ∘ i1) B = j1 ∧ restr (H ∘ i2) C = j2

cardgt0

⊢ cardgt (:α) 0

cardgt1_INJ_bool

⊢ cardgt (:α) 1 ⇔ ∃bf. INJ bf 𝟚 𝕌(:α)

eps_partition

⊢ a ∈ A ⇒ eps R A a ∈ partition R A

kernel_graph

⊢ kernel A f = (Gr f A)ᵀ ∘ᵣ Gr f A

oID

⊢ f ∘ (λx. x) = f ∧ (λx. x) ∘ f = f

restr_EMPTY

⊢ restr f ∅ = K ARB

restr_applies

⊢ x ∈ A ⇒ restr f A x = f x

restr_cases

⊢ restr f A x = g x ⇔ x ∈ A ∧ f x = g x ∨ x ∉ A ∧ g x = ARB

restr_restr_o

⊢ restr (f ∘ restr g A) A = restr (f ∘ g) A

shom_into_EMPTY

⊢ shom f A ∅ ⇔ A = ∅ ∧ f = K ARB

shom_outof_EMPTY

⊢ shom f ∅ A ⇔ f = K ARB

shoms_exist

⊢ ∀A B. B ≠ ∅ ⇒ ∃h. shom h A B

symmetric_SPOr

⊢ symmetric (SPOr A f g)

transitive_SPOr

⊢ transitive (SPOr A f g)

unit_pushout

⊢ shom f A B ∧ shom g A C ∧ A ≠ ∅ ⇒
  Spushout A B C f g ({()},restr (K ()) B,restr (K ()) C) (:unit)

Theory simpleSetCat

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems