The Theory sets
Parents
basic_hol
Children
orders set_thms hol
Constants
IsSetRep
('a → BOOL) → BOOL
$SetComp
('a → BOOL) → 'a SET
$∈
'a → 'a SET → BOOL
{}
'a SET
Universe
'a SET
Insert
'a → 'a SET → 'a SET
~
'a SET → 'a SET
$∪
'a SET → 'a SET → 'a SET
$∩
'a SET → 'a SET → 'a SET
$\
'a SET → 'a SET → 'a SET
$⊖
'a SET → 'a SET → 'a SET
$⊆
'a SET → 'a SET → BOOL
$⊂
'a SET → 'a SET → BOOL
'a SET SET → 'a SET
'a SET SET → 'a SET
'a SET → 'a SET SET
Types
'1 SET
Fixity
Binder: SetComp
Left Infix 265:
\
Right Infix 230:

Right Infix 250:

Right Infix 260:

Right Infix 270:

Definitions
IsSetRep
is_set_rep_def
⊢ IsSetRep = (λ x• T)
SET
set_def
⊢ ∃ f• TypeDefn IsSetRep f
SetComp
set_comp_def
⊢ ∀ x p a b
fill• (x ∈ {v|p v} ⇔ p x)
fill∧ (a = b ⇔ (∀ x• x ∈ a ⇔ x ∈ b))
Empty
Universe
Insert
insert_def
⊢ ∀ x y a
fill• ¬ x ∈ {}
fill∧ x ∈ Universe
fill∧ (x ∈ Insert y a ⇔ x = y ∨ x ∈ a)
~
complement_def
⊢ ∀ x a• x ∈ ~ a ⇔ ¬ x ∈ a
∪_def
⊢ ∀ x a b• x ∈ a ∪ b ⇔ x ∈ a ∨ x ∈ b
∩_def
⊢ ∀ x a b• x ∈ a ∩ b ⇔ x ∈ a ∧ x ∈ b
\
set_dif_def
⊢ ∀ x a b• x ∈ a \ b ⇔ x ∈ a ∧ ¬ x ∈ b
⊖_def
⊢ ∀ x a b• x ∈ a ⊖ b ⇔ ¬ (x ∈ a ⇔ x ∈ b)
⊆_def
⊢ ∀ a b• a ⊆ b ⇔ (∀ x• x ∈ a ⇒ x ∈ b)
⊂_def
⊢ ∀ a b• a ⊂ b ⇔ a ⊆ b ∧ (∃ x• ¬ x ∈ a ∧ x ∈ b)
⋃_def
⊢ ∀ x a• x ∈ ⋃ a ⇔ (∃ s• x ∈ s ∧ s ∈ a)
⋂_def
⊢ ∀ x a• x ∈ ⋂ a ⇔ (∀ s• s ∈ a ⇒ x ∈ s)
℘_def
⊢ ∀ x a• x ∈ ℘ a ⇔ x ⊆ a
Theorems
sets_clauses
⊢ ∀ x y p q
fill• (x ∈ {} ⇔ F)
fill∧ (x ∈ Universe ⇔ T)
fill∧ (x ∈ {v|q} ⇔ q)
fill∧ (x ∈ {v|p v} ⇔ p x)
fill∧ (x ∈ {v|v = y} ⇔ x = y)
fill∧ (x ∈ {y} ⇔ x = y)
complement_clauses
⊢ (∀ x a• x ∈ ~ a ⇔ ¬ x ∈ a)
fill∧ ~ Universe = {}
fill∧ ~ {} = Universe
∪_clauses
⊢ ∀ a
fill• a ∪ {} = a
fill∧ {} ∪ a = a
fill∧ a ∪ Universe = Universe
fill∧ Universe ∪ a = Universe
fill∧ a ∪ a = a
∩_clauses
⊢ ∀ a
fill• a ∩ {} = {}
fill∧ {} ∩ a = {}
fill∧ a ∩ Universe = a
fill∧ Universe ∩ a = a
fill∧ a ∩ a = a
set_dif_clauses
⊢ ∀ a
fill• a \ {} = a
fill∧ {} \ a = {}
fill∧ a \ Universe = {}
fill∧ Universe \ a = ~ a
fill∧ a \ a = {}
⊖_clauses
⊢ ∀ a
fill• a ⊖ {} = a
fill∧ {} ⊖ a = a
fill∧ a ⊖ Universe = ~ a
fill∧ Universe ⊖ a = ~ a
fill∧ a ⊖ a = {}
⊆_clauses
⊢ ∀ a• a ⊆ a ∧ {} ⊆ a ∧ a ⊆ Universe
⊂_clauses
⊢ ∀ a• ¬ a ⊂ a ∧ ¬ a ⊂ {} ∧ {} ⊂ Universe
⋃_clauses
⊢ ⋃ {} = {} ∧ ⋃ Universe = Universe
⋂_clauses
⊢ ⋂ {} = Universe ∧ ⋂ Universe = {}
℘_clauses
⊢ ∀ a
fill• ℘ {} = {{}}
fill∧ ℘ Universe = Universe
fill∧ a ∈ ℘ a
fill∧ {} ∈ ℘ a
∅_clauses
⊢ ∀ x a
fill• {x|F} = {}
fill∧ ¬ x ∈ {}
fill∧ {} ∪ a = a
fill∧ a ∪ {} = a
fill∧ {} ∩ a = {}
fill∧ a ∩ {} = {}
fill∧ a \ {} = a
fill∧ {} \ a = {}
fill∧ a ⊖ {} = a
fill∧ {} ⊖ a = a
fill∧ {} ⊆ a
fill∧ (a ⊆ {} ⇔ a = {})
fill∧ ({} ⊂ a ⇔ ¬ a = {})
fill∧ ¬ a ⊂ {}
fill∧ ¬ x ∈ ⋃ {}
fill∧ x ∈ ⋂ {}
fill∧ {} ∈ ℘ a
fill∧ ℘ {} = {{}}
∈_in_clauses
⊢ (∀ x y a
fill• (x ∈ Universe ⇔ T)
fill∧ (x ∈ {} ⇔ F)
fill∧ (x ∈ Insert y a ⇔ x = y ∨ x ∈ a))
fill∧ (∀ x a b
fill• (x ∈ a ∪ b ⇔ x ∈ a ∨ x ∈ b)
fill∧ (x ∈ a ∩ b ⇔ x ∈ a ∧ x ∈ b)
fill∧ (x ∈ a \ b ⇔ x ∈ a ∧ ¬ x ∈ b)
fill∧ (x ∈ a ⊖ b ⇔ ¬ (x ∈ a ⇔ x ∈ b)))
fill∧ (∀ x a
fill• (x ∈ ⋃ a ⇔ (∃ s• x ∈ s ∧ s ∈ a))
fill∧ (x ∈ ⋂ a ⇔ (∀ s• s ∈ a ⇒ x ∈ s))
fill∧ (∀ x a• x ∈ ℘ a ⇔ x ⊆ a))
sets_ext_clauses
⊢ ∀ a b
fill• (a ⊂ b
fill⇔ (∀ x• x ∈ a ⇒ x ∈ b)
fill∧ (∃ x• ¬ x ∈ a ∧ x ∈ b))
fill∧ (a ⊆ b ⇔ (∀ x• x ∈ a ⇒ x ∈ b))
fill∧ (a = b ⇔ (∀ x• x ∈ a ⇔ x ∈ b))

up quick index

privacy policy

Created:

V