Nuprl Lemma : weak-antecedent-surjection-property

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


Proof




Definitions occuring in Statement :  weak-antecedent-surjection: Q ←←f== P es-E: E event_ordering: EO uimplies: supposing a uall: [x:A]. B[x] prop: member: t ∈ T set: {x:A| B[x]}  apply: a function: x:A ─→ B[x]
Lemmas :  weak-antecedent-function-property weak-antecedent-surjection_wf es-E_wf event_ordering_wf
\mforall{}[es:EO].  \mforall{}[P,Q:E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[f:\{e:E|  P  e\}    {}\mrightarrow{}  E].    f  \mmember{}  \{e:E|  P  e\}    {}\mrightarrow{}  \{e:E|  Q  e\}    supposing  Q  \mleftarrow{}\mleftarrow{}=  f==  \000CP



Date html generated: 2015_07_17-AM-09_02_23
Last ObjectModification: 2015_01_27-PM-00_55_09

Home Index