Nuprl Lemma : fl-filter-filter
∀[P,Q,s:Top].  (fl-filter(fl-filter(s;x.P[x]);x.Q[x]) ~ fl-filter(s;x.P[x] ∧b Q[x]))
Proof
Definitions occuring in Statement : 
fl-filter: fl-filter(s;x.Q[x])
, 
band: p ∧b q
, 
uall: ∀[x:A]. B[x]
, 
top: Top
, 
so_apply: x[s]
, 
sqequal: s ~ t
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
fl-filter: fl-filter(s;x.Q[x])
, 
cal-filter: cal-filter(s;x.P[x])
, 
fset-filter: {x ∈ s | P[x]}
, 
top: Top
Lemmas referenced : 
top_wf, 
filter-filter
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
introduction, 
cut, 
sqequalRule, 
lemma_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
isect_memberEquality, 
voidElimination, 
voidEquality, 
hypothesisEquality, 
hypothesis, 
sqequalAxiom, 
because_Cache
Latex:
\mforall{}[P,Q,s:Top].    (fl-filter(fl-filter(s;x.P[x]);x.Q[x])  \msim{}  fl-filter(s;x.P[x]  \mwedge{}\msubb{}  Q[x]))
Date html generated:
2016_05_18-AM-11_40_50
Last ObjectModification:
2016_01_15-PM-05_52_25
Theory : lattices
Home
Index