Nuprl Lemma : bag-filter-singleton
∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[v:T].  ([x∈{v}|p[x]] ~ if p[v] then {v} else {} fi )
Proof
Definitions occuring in Statement : 
bag-filter: [x∈b|p[x]]
, 
single-bag: {x}
, 
empty-bag: {}
, 
ifthenelse: if b then t else f fi 
, 
bool: 𝔹
, 
uall: ∀[x:A]. B[x]
, 
so_apply: x[s]
, 
function: x:A ⟶ B[x]
, 
universe: Type
, 
sqequal: s ~ t
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
empty-bag: {}
, 
single-bag: {x}
, 
bag-filter: [x∈b|p[x]]
, 
all: ∀x:A. B[x]
, 
top: Top
Lemmas referenced : 
filter_cons_lemma, 
filter_nil_lemma, 
bool_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
introduction, 
cut, 
sqequalRule, 
lemma_by_obid, 
sqequalHypSubstitution, 
dependent_functionElimination, 
thin, 
isect_memberEquality, 
voidElimination, 
voidEquality, 
hypothesis, 
sqequalAxiom, 
hypothesisEquality, 
isectElimination, 
because_Cache, 
functionEquality, 
universeEquality
Latex:
\mforall{}[T:Type].  \mforall{}[p:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[v:T].    ([x\mmember{}\{v\}|p[x]]  \msim{}  if  p[v]  then  \{v\}  else  \{\}  fi  )
Date html generated:
2016_05_15-PM-02_23_16
Last ObjectModification:
2015_12_27-AM-09_54_19
Theory : bags
Home
Index