Nuprl Lemma : bmsexists_char_rw

s:DSet. ∀f:|s| ⟶ 𝔹. ∀a:MSet{s}.  {(∃x:|s|. ((↑(x ∈b a)) ∧ (↑f[x])))  (↑(∃b{s} x ∈ a. f[x]))}


Proof




Definitions occuring in Statement :  mset_for: mset_for mset_mem: mset_mem mset: MSet{s} assert: b bool: 𝔹 guard: {T} so_apply: x[s] all: x:A. B[x] exists: x:A. B[x] implies:  Q and: P ∧ Q function: x:A ⟶ B[x] bor_mon: <𝔹,∨b> dset: DSet set_car: |p|
Definitions unfolded in proof :  guard: {T}
Lemmas referenced :  bmsexists_char
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lemma_by_obid

Latex:
\mforall{}s:DSet.  \mforall{}f:|s|  {}\mrightarrow{}  \mBbbB{}.  \mforall{}a:MSet\{s\}.    \{(\mexists{}x:|s|.  ((\muparrow{}(x  \mmember{}\msubb{}  a))  \mwedge{}  (\muparrow{}f[x])))  {}\mRightarrow{}  (\muparrow{}(\mexists{}\msubb{}\{s\}  x  \mmember{}  a.  f[x]))\}



Date html generated: 2016_05_16-AM-07_48_06
Last ObjectModification: 2015_12_28-PM-06_02_41

Theory : mset


Home Index