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: 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 ∈ 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