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