Nuprl Lemma : lg-all-map
∀[A,T:Type]. ∀f:A ─→ T. ∀[P:T ─→ ℙ]. ∀g:LabeledGraph(A). (∀x∈lg-map(f;g).P[x] ⇐⇒ ∀x∈g.P[f x])
Proof
Definitions occuring in Statement :
lg-all: ∀x∈G.P[x],
lg-map: lg-map(f;g),
labeled-graph: LabeledGraph(T),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
apply: f a,
function: x:A ─→ B[x],
universe: Type
Lemmas :
length-map-sq,
dep-isect-subtype,
list_wf,
top_wf,
int_seg_wf,
length_wf,
select-map,
lelt_wf,
lg-size_wf,
select_wf,
nat_wf,
sq_stable__le,
lg-all_wf,
lg-map_wf,
labeled-graph_wf
Latex:
\mforall{}[A,T:Type]. \mforall{}f:A {}\mrightarrow{} T. \mforall{}[P:T {}\mrightarrow{} \mBbbP{}]. \mforall{}g:LabeledGraph(A). (\mforall{}x\mmember{}lg-map(f;g).P[x] \mLeftarrow{}{}\mRightarrow{} \mforall{}x\mmember{}g.P[f x])
Date html generated:
2015_07_23-AM-11_04_49
Last ObjectModification:
2015_01_28-PM-11_35_10
Home
Index