Nuprl Lemma : antecedent-surjection_wf

[es:EO]. ∀[P,Q:E ─→ ℙ]. ∀[f:{e:E| e}  ─→ {e:E| e} ].  (Q ←←─ f── P ∈ ℙ)


Proof




Definitions occuring in Statement :  antecedent-surjection: Q ←←─ f── P es-E: E event_ordering: EO uall: [x:A]. B[x] prop: member: t ∈ T set: {x:A| B[x]}  apply: a function: x:A ─→ B[x]
Lemmas :  antecedent-function_wf all_wf es-E_wf exists_wf equal_wf event_ordering_wf
\mforall{}[es:EO].  \mforall{}[P,Q:E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[f:\{e:E|  P  e\}    {}\mrightarrow{}  \{e:E|  Q  e\}  ].    (Q  \mleftarrow{}\mleftarrow{}{}  f{}{}  P  \mmember{}  \mBbbP{})



Date html generated: 2015_07_17-AM-09_06_31
Last ObjectModification: 2015_01_27-PM-00_48_36

Home Index