### Nuprl Lemma : bmsexists_char_a_rw

`∀s:DSet. ∀f:|s| ⟶ 𝔹. ∀a:MSet{s}.  {(↑(∃b{s} x ∈ a. f[x])) `` (↓∃x:|s|. ((↑(x ∈b 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]` squash: `↓T` implies: `P `` 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_a
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\}.    \{(\muparrow{}(\mexists{}\msubb{}\{s\}  x  \mmember{}  a.  f[x]))  {}\mRightarrow{}  (\mdownarrow{}\mexists{}x:|s|.  ((\muparrow{}(x  \mmember{}\msubb{}  a))  \mwedge{}  (\muparrow{}f[x])))\}

Date html generated: 2016_05_16-AM-07_48_04
Last ObjectModification: 2015_12_28-PM-06_02_43

Theory : mset

Home Index