The Theory gst-fun
Parents
gst-ax
Constants
$↦g
GS → GS → GS
snd
GS → GS
fst
GS → GS
g
GS → GS → GS
$↔g
GS → GS → GS
rel
GS → BOOL
$og
GS → GS → GS
dom
GS → GS
ran
GS → GS
field
GS → GS
fun
GS → BOOL
$g
GS → GS → GS
$→g
GS → GS → GS
g
(GS → GS) → GS → GS
$g
GS → GS → GS
id
GS → GS
Fixity
Binder: λg
Right Infix 240:
g g ×g g g
Right Infix 250:
og g
Definitions
g
⊢ ∀ s t u v
fill• (s ↦g t = u ↦g v ⇔ s = u ∧ t = v)
fill∧ Pairg s t ∈g Gx (s ↦g t)
fst
snd
⊢ ∀ s t• fst (s ↦g t) = s ∧ snd (s ↦g t) = t
×g
⊢ ∀ s t e
fill• e ∈g s ×g t
fill⇔ (∃ l r• l ∈g s ∧ r ∈g t ∧ e = l ↦g r)
g
⊢ ∀ s t• s ↔g t = ℘g (s ×g t)
rel
⊢ ∀ x• rel x ⇔ (∀ y• y ∈g x ⇒ (∃ s t• y = s ↦g t))
og
⊢ ∀ f g
fill• f og g
fill= Imagep
fill(λ p• fst (fst p) ↦g snd (snd p))
fill(Sep
fill(g ×g f)
fill(λ p• ∃ q r s• p = (q ↦g r) ↦g r ↦g s))
dom
⊢ ∀ x• dom x = Sep (Gx x) (λ w• ∃ v• w ↦g v ∈g x)
ran
⊢ ∀ x• ran x = Sep (Gx x) (λ w• ∃ v• v ↦g w ∈g x)
field
⊢ ∀ s e• e ∈g field s ⇔ e ∈g dom s ∨ e ∈g ran s
fun
⊢ ∀ x
fill• fun x
fill⇔ rel x
fill∧ (∀ s t u
fill• s ↦g u ∈g x ∧ s ↦g t ∈g x ⇒ u = t)
g
⊢ ∀ s t• s g t = Sep (s ↔g t) fun
g
⊢ ∀ s t• s →g t = Sep (s g t) (λ r• dom r = s)
λg
⊢ ∀ f s
fill• $λg f s
fill= Sep (s ×g Imagep f s) (λ p• snd p = f (fst p))
g
⊢ ∀ f x
fill• f g x
fill= (if ∃ y• x ↦g y ∈g f
fillthen ε y• x ↦g y ∈g f
fillelse f)
id
⊢ ∀ s• id s = Sep (s ×g s) (λ x• fst x = snd x)
Theorems
f↦gs_thm
⊢ ∀ s t p• p ∈g s ×g t ⇒ fst p ↦g snd p = p
v∈g×g_thm
⊢ ∀ p s t• p ∈g s ×g t ⇒ fst p ∈g s ∧ snd p ∈g t
gg×g_thm
⊢ ∀ l r s t• l ↦g r ∈g s ×g t ⇔ l ∈g s ∧ r ∈g t
gg×g_thm
⊢ ∀ s t r• r ∈g s ↔g t ⇔ r ⊆g s ×g t
ggg_thm
⊢ ∀ s t• ∅gg s ↔g t
f↦gs_thm1
⊢ ∀ p r s t
fill• p ∈g r ∧ r ∈g s ↔g t ⇒ fst p ↦g snd p = p
gg_thm
⊢ ∀ p r s t
fill• p ∈g r ∧ r ∈g s ↔g t ⇒ fst p ∈g s ∧ snd p ∈g t
rel_∅g_thm
⊢ rel ∅g
og_thm
⊢ ∀ f g x
fill• x ∈g f og g
fill⇔ (∃ q r s
fill• q ↦g r ∈g g ∧ r ↦g s ∈g f ∧ x = q ↦g s)
og_thm2
⊢ ∀ f g x y
fill• x ↦g y ∈g f og g
fill⇔ (∃ z• x ↦g z ∈g g ∧ z ↦g y ∈g f)
og_rel_thm
⊢ ∀ r s• rel r ∧ rel s ⇒ rel (r og s)
og_associative_thm
⊢ ∀ f g h• (f og g) og h = f og g og h
dom_∅g_thm
⊢ dom ∅g = ∅g
dom_thm
⊢ ∀ r y• y ∈g dom r ⇔ (∃ x• y ↦g x ∈g r)
ran_∅g_thm
⊢ ran ∅g = ∅g
ran_thm
⊢ ∀ r y• y ∈g ran r ⇔ (∃ x• x ↦g y ∈g r)
rel_sub_cp_thm
⊢ ∀ x• rel x ⇔ (∃ s t• x ⊆g s ×g t)
field_∅g_thm
⊢ field ∅g = ∅g
fun_∅g_thm
⊢ fun ∅g
og_fun_thm
⊢ ∀ f g• fun f ∧ fun g ⇒ fun (f og g)
ran_og_thm
⊢ ∀ f g• ran (f og g) ⊆g ran f
dom_og_thm
⊢ ∀ f g• dom (f og g) ⊆g dom g
dom_og_thm2
⊢ ∀ f g• ran g ⊆g dom f ⇒ dom (f og g) = dom g
ggg_thm
⊢ ∀ s t• ∅gg s g t
g_thm
⊢ ∀ s t• ∃ f• f ∈g s g t
gggg_thm
⊢ ∀ s t• ∅gggg t
∃→g_thm
⊢ ∀ s t• (∃ x• x ∈g t) ⇒ (∃ f• f ∈g s →g t)
app_thm1
⊢ ∀ f x• (∃1 y• x ↦g y ∈g f) ⇒ x ↦g f g x ∈g f
app_thm2
⊢ ∀ f x y• fun f ∧ x ↦g y ∈g f ⇒ f g x = y
app_thm3
⊢ ∀ f x• fun f ∧ x ∈g dom f ⇒ x ↦g f g x ∈g f
og_g_thm
⊢ ∀ f g x
fill• fun f ∧ fun g ∧ x ∈g dom g ∧ ran g ⊆g dom f
fill⇒ (f og g) g x = f g g g x
gg_thm
⊢ ∀ f s t u• f ∈g s g t ∧ u ∈g dom f ⇒ f g u ∈g t
gg_thm1
⊢ ∀ f s t u• f ∈g s →g t ∧ u ∈g s ⇒ f g u ∈g t
gg⇒∈gg_thm
⊢ ∀ f s t u• f ∈g s g t ⇒ f ∈g dom f →g t
id_thm1
⊢ ∀ s x• x ∈g id s ⇔ (∃ y• y ∈g s ∧ x = y ↦g y)
id_ap_thm
⊢ ∀ s x• x ∈g s ⇒ id s g x = x
id∈gg_thm1
⊢ ∀ s t u• s ⊆g t ∩g u ⇒ id s ∈g t g u
id∈gg_thm2
⊢ ∀ s t u• s ⊆g t ⇒ id s ∈g t g t
id_clauses
⊢ ∀ s
fill• rel (id s)
fill∧ fun (id s)
fill∧ dom (id s) = s
fill∧ ran (id s) = s

up quick index

privacy policy

Created:

V