Nuprl Lemma : member-fset-filter
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)]. ∀[x:T]. uiff(x ∈ {x ∈ s | P[x]};{x ∈ s ∧ (↑P[x])})
Proof
Definitions occuring in Statement :
fset-filter: {x ∈ s | P[x]},
fset-member: a ∈ s,
fset: fset(T),
deq: EqDecider(T),
assert: ↑b,
bool: 𝔹,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
guard: {T},
so_apply: x[s],
and: P ∧ Q,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uiff: uiff(P;Q),
and: P ∧ Q,
uimplies: b supposing a,
guard: {T},
so_apply: x[s],
prop: ℙ,
implies: P ⇒ Q,
all: ∀x:A. B[x],
decidable: Dec(P),
or: P ∨ Q,
fset: fset(T),
quotient: x,y:A//B[x; y],
not: ¬A,
fset-filter: {x ∈ s | P[x]},
fset-member: a ∈ s,
iff: P ⇐⇒ Q,
cand: A c∧ B,
rev_implies: P ⇐ Q,
false: False,
sq_type: SQType(T),
true: True,
so_lambda: λ2x.t[x]
Lemmas referenced :
decidable__and2,
fset-member_wf,
assert_wf,
decidable__fset-member,
decidable__assert,
list_wf,
set-equal_wf,
set-equal-reflex,
assert-deq-member,
filter_wf5,
l_member_wf,
member_filter,
equal-wf-base,
equal_wf,
subtype_base_sq,
int_subtype_base,
fset-member_witness,
assert_witness,
fset-filter_wf,
fset_wf,
bool_wf,
deq_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
independent_pairFormation,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
cumulativity,
hypothesisEquality,
hypothesis,
isect_memberEquality,
applyEquality,
functionExtensionality,
independent_functionElimination,
because_Cache,
dependent_functionElimination,
lambdaFormation,
unionElimination,
promote_hyp,
equalityTransitivity,
equalitySymmetry,
pointwiseFunctionality,
sqequalRule,
pertypeElimination,
productElimination,
lambdaEquality,
setElimination,
rename,
setEquality,
voidElimination,
productEquality,
intEquality,
natural_numberEquality,
instantiate,
independent_isectElimination,
independent_pairEquality,
functionEquality,
universeEquality
Latex:
\mforall{}[T:Type]. \mforall{}[eq:EqDecider(T)]. \mforall{}[P:T {}\mrightarrow{} \mBbbB{}]. \mforall{}[s:fset(T)]. \mforall{}[x:T].
uiff(x \mmember{} \{x \mmember{} s | P[x]\};\{x \mmember{} s \mwedge{} (\muparrow{}P[x])\})
Date html generated:
2017_04_17-AM-09_19_15
Last ObjectModification:
2017_02_27-PM-05_22_36
Theory : finite!sets
Home
Index