Nuprl Lemma : fpf-union-contains2

`∀[A,V:Type]. ∀[B:A ⟶ Type].`
`  ∀eq:EqDecider(A). ∀f,g:x:A fp-> B[x] List.`
`    ∀x:A. ∀R:(V List) ⟶ V ⟶ 𝔹.  (fpf-union-compatible(A;V;x.B[x];eq;R;f;g) `` g(x)?[] ⊆ fpf-union(f;g;eq;R;x)) `
`    supposing fpf-single-valued(A;eq;x.B[x];V;g) `
`  supposing ∀a:A. (B[a] ⊆r V)`

Proof

Definitions occuring in Statement :  fpf-single-valued: `fpf-single-valued(A;eq;x.B[x];V;g)` fpf-union-compatible: `fpf-union-compatible(A;C;x.B[x];eq;R;f;g)` fpf-union: `fpf-union(f;g;eq;R;x)` fpf-cap: `f(x)?z` fpf: `a:A fp-> B[a]` l_contains: `A ⊆ B` nil: `[]` list: `T List` deq: `EqDecider(T)` bool: `𝔹` uimplies: `b supposing a` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` all: `∀x:A. B[x]` subtype_rel: `A ⊆r B` fpf-single-valued: `fpf-single-valued(A;eq;x.B[x];V;g)` implies: `P `` Q` prop: `ℙ` so_apply: `x[s]` so_lambda: `λ2x.t[x]` top: `Top` fpf-union: `fpf-union(f;g;eq;R;x)` fpf-cap: `f(x)?z` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` ifthenelse: `if b then t else f fi ` band: `p ∧b q` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` l_contains: `A ⊆ B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` decidable: `Dec(P)` cand: `A c∧ B` fpf-union-compatible: `fpf-union-compatible(A;C;x.B[x];eq;R;f;g)` label: `...\$L... t`
Lemmas referenced :  equal_wf l_member_wf fpf-ap_wf list_wf assert_wf fpf-dom_wf subtype-fpf2 top_wf bool_wf eqtt_to_assert eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot l_contains_weakening l_contains_nil nil_wf fpf-union-compatible_wf fpf-single-valued_wf fpf_wf deq_wf all_wf subtype_rel_wf l_all_iff append_wf filter_wf5 subtype_rel_list subtype_rel_dep_function subtype_rel_transitivity subtype_rel_self set_wf member_append decidable__assert member_filter or_wf l_member_subtype not_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality axiomEquality hypothesis rename lambdaFormation extract_by_obid isectElimination cumulativity applyEquality functionExtensionality independent_isectElimination isect_memberEquality voidElimination voidEquality because_Cache unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination dependent_pairFormation promote_hyp instantiate independent_functionElimination functionEquality universeEquality setElimination setEquality inrFormation independent_pairFormation inlFormation productEquality addLevel orFunctionality hyp_replacement applyLambdaEquality

Latex:
\mforall{}[A,V:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
\mforall{}eq:EqDecider(A).  \mforall{}f,g:x:A  fp->  B[x]  List.
\mforall{}x:A.  \mforall{}R:(V  List)  {}\mrightarrow{}  V  {}\mrightarrow{}  \mBbbB{}.
(fpf-union-compatible(A;V;x.B[x];eq;R;f;g)  {}\mRightarrow{}  g(x)?[]  \msubseteq{}  fpf-union(f;g;eq;R;x))
supposing  fpf-single-valued(A;eq;x.B[x];V;g)
supposing  \mforall{}a:A.  (B[a]  \msubseteq{}r  V)

Date html generated: 2018_05_21-PM-09_18_31
Last ObjectModification: 2018_02_09-AM-10_17_10

Theory : finite!partial!functions

Home Index