Theory "res_quan"

Theorems

RES_SELECT_UNIV

|- ∀p. RES_SELECT 𝕌(:α) p = $@ p

RES_SELECT_EMPTY

|- ∀p. RES_SELECT ∅ p = @x. F

RES_EXISTS_UNIQUE_ALT

|- ∀p m. RES_EXISTS_UNIQUE p m ⇔ ∃x::p. m x ∧ ∀y::p. m y ⇒ (y = x)

RES_EXISTS_UNIQUE_NULL

|- ∀p m. (∃!x::p. m) ⇔ (∃x. p = {x}) ∧ m

RES_EXISTS_UNIQUE_UNIV

|- ∀p. RES_EXISTS_UNIQUE 𝕌(:α) p ⇔ $?! p

RES_EXISTS_UNIQUE_EMPTY

|- ∀p. ¬RES_EXISTS_UNIQUE ∅ p

RES_EXISTS_ALT

|- ∀p m. RES_EXISTS p m ⇔ RES_SELECT p m ∈ p ∧ m (RES_SELECT p m)

RES_EXISTS_NULL

|- ∀p m. (∃x::p. m) ⇔ p ≠ ∅ ∧ m

RES_EXISTS_UNIV

|- ∀p. RES_EXISTS 𝕌(:α) p ⇔ $? p

RES_EXISTS_EMPTY

|- ∀p. ¬RES_EXISTS ∅ p

RES_EXISTS_REORDER

|- ∀P Q R. (∃(i::P) (j::Q). R i j) ⇔ ∃(j::Q) (i::P). R i j

RES_EXISTS_EQUAL

|- ∀P j. (∃i:: $= j. P i) ⇔ P j

RES_DISJ_EXISTS_DIST

|- ∀P Q R. (∃i::(λi. P i ∨ Q i). R i) ⇔ (∃i::P. R i) ∨ ∃i::Q. R i

RES_EXISTS_DISJ_DIST

|- ∀P Q R. (∃i::P. Q i ∨ R i) ⇔ (∃i::P. Q i) ∨ ∃i::P. R i

RES_FORALL_NULL

|- ∀p m. (∀x::p. m) ⇔ (p = ∅) ∨ m

RES_FORALL_UNIV

|- ∀p. RES_FORALL 𝕌(:α) p ⇔ $! p

RES_FORALL_EMPTY

|- ∀p. RES_FORALL ∅ p

RES_FORALL_REORDER

|- ∀P Q R. (∀(i::P) (j::Q). R i j) ⇔ ∀(j::Q) (i::P). R i j

RES_FORALL_FORALL

|- ∀P R x. (∀x (i::P). R i x) ⇔ ∀(i::P) x. R i x

RES_FORALL_UNIQUE

|- ∀P j. (∀i:: $= j. P i) ⇔ P j

RES_FORALL_DISJ_DIST

|- ∀P Q R. (∀i::(λj. P j ∨ Q j). R i) ⇔ (∀i::P. R i) ∧ ∀i::Q. R i

RES_FORALL_CONJ_DIST

|- ∀P Q R. (∀i::P. Q i ∧ R i) ⇔ (∀i::P. Q i) ∧ ∀i::P. R i

RES_FORALL

|- ∀P f. RES_FORALL P f ⇔ ∀x. x ∈ P ⇒ f x

RES_EXISTS

|- ∀P f. RES_EXISTS P f ⇔ ∃x. x ∈ P ∧ f x

RES_EXISTS_UNIQUE

|- ∀P f. RES_EXISTS_UNIQUE P f ⇔ (∃x::P. f x) ∧ ∀x y::P. f x ∧ f y ⇒ (x = y)

RES_SELECT

|- ∀P f. RES_SELECT P f = @x. x ∈ P ∧ f x

RES_ABSTRACT

|- ∀p m x. x ∈ p ⇒ (RES_ABSTRACT p m x = m x)

RES_ABSTRACT_EQUAL

|- ∀p m1 m2.
     (∀x. x ∈ p ⇒ (m1 x = m2 x)) ⇒ (RES_ABSTRACT p m1 = RES_ABSTRACT p m2)

RES_ABSTRACT_IDEMPOT

|- ∀p m. RES_ABSTRACT p (RES_ABSTRACT p m) = RES_ABSTRACT p m

RES_ABSTRACT_EQUAL_EQ

|- ∀p m1 m2.
     (RES_ABSTRACT p m1 = RES_ABSTRACT p m2) ⇔ ∀x. x ∈ p ⇒ (m1 x = m2 x)