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