Theory "fsets"

Signature

Definitions

FSET_def

⊢ ∀AB fs s. FSET AB fs s ⇔ ∀a b. AB a b ⇒ (fIN a fs ⇔ b ∈ s)

Theorems

KT_FINITE

⊢ surj AB ∧ right_unique AB ⇒ (FSET AB |==> $<=>) (K T) FINITE

RDOM_FSET_EQ

⊢ RDOM (FSET $=) = 𝕌(:α fset)

RRANGE_FSET

⊢ RRANGE (FSET AB) =
  {bset |
   FINITE {a | (∃b. AB a b ∧ b ∈ bset)} ∧
   ∀a b b'. b ∈ bset ∧ AB a b ∧ AB a b' ⇒ b' ∈ bset}

RRANGE_FSET_EQ

⊢ RRANGE (FSET $=) = FINITE

bi_unique_FSET

⊢ bi_unique AB ∧ bitotal AB ⇒ bi_unique (FSET AB)

fDELETE_DELETE

⊢ bi_unique AB ⇒ (FSET AB |==> AB |==> FSET AB) fDELETE $DELETE

fEMPTY_EMPTY

⊢ FSET AB FEMPTY ∅

fINSERT_INSERT

⊢ bi_unique AB ⇒ (AB |==> FSET AB |==> FSET AB) (λe fs. fINSERT e fs) $INSERT

fIN_IN

⊢ (AB |==> FSET AB |==> $<=>) (λe fs. fIN e fs) $IN

fUNION_UNION

⊢ (FSET AB |==> FSET AB |==> FSET AB) fUNION $UNION

fset_ext

⊢ (fm1 = fm2) ⇔ (toSet fm1 = toSet fm2)

fupdate_correct

⊢ bi_unique AB ⇒ (FSET AB |==> PAIRU AB |==> FSET AB) $|+ (flip $INSERT)

left_unique_FSET

⊢ total AB ⇒ left_unique (FSET AB)

right_unique_FSET

⊢ surj AB ⇒ right_unique (FSET AB)

toSet_correct

⊢ (FSET AB |==> AB |==> $<=>) toSet I

total_FSET

⊢ left_unique AB ⇒ total (FSET AB)