Nuprl Lemma : fset-ac-lub-is-lub

[T:Type]. ∀[eq:EqDecider(T)]. ∀[ac1,ac2:{ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ].
  least-upper-bound({ac:fset(fset(T))| ↑fset-antichain(eq;ac)} ;ac1,ac2.fset-ac-le(eq;ac1;ac2);
                    ac1;ac2;fset-ac-lub(eq;ac1;ac2))


Proof




Definitions occuring in Statement :  fset-ac-lub: fset-ac-lub(eq;ac1;ac2) fset-ac-le: fset-ac-le(eq;ac1;ac2) fset-antichain: fset-antichain(eq;ac) fset: fset(T) deq: EqDecider(T) least-upper-bound: least-upper-bound(T;x,y.R[x; y];a;b;c) assert: b uall: [x:A]. B[x] set: {x:A| B[x]}  universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T least-upper-bound: least-upper-bound(T;x,y.R[x; y];a;b;c) and: P ∧ Q fset-ac-lub: fset-ac-lub(eq;ac1;ac2) so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] uimplies: supposing a all: x:A. B[x] cand: c∧ B squash: T prop: true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q fset-ac-le: fset-ac-le(eq;ac1;ac2) fset-all: fset-all(s;x.P[x]) so_lambda: λ2x.t[x] so_apply: x[s] uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) not: ¬A or: P ∨ Q
Lemmas referenced :  member-fset-union member-fset-minimals empty-fset_wf equal_wf not_wf assert-fset-null assert_of_bnot fset-member_wf isect_wf uall_wf fset-all_wf iff_weakening_uiff fset-all-iff deq_wf set_wf fset-antichain_wf fset-ac-lub_wf assert_wf iff_wf all_wf bool_wf deq-f-subset_wf bnot_wf fset-filter_wf fset-null_wf assert_witness fset-ac-le_wf fset-ac-le-implies iff_weakening_equal fset-union-commutes true_wf squash_wf f-subset_wf f-subset-union fset-ac-le_weakening_f-subset fset-minimals-ac-le f-proper-subset-dec_wf fset-minimals_wf deq-fset_wf fset_wf fset-union_wf fset-ac-le_transitivity
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename sqequalRule lambdaEquality independent_isectElimination dependent_functionElimination because_Cache applyEquality imageElimination equalityTransitivity equalitySymmetry natural_numberEquality imageMemberEquality baseClosed universeEquality productElimination independent_functionElimination lambdaFormation independent_pairEquality setEquality functionEquality cumulativity isect_memberEquality addLevel impliesFunctionality unionElimination

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[ac1,ac2:\{ac:fset(fset(T))|  \muparrow{}fset-antichain(eq;ac)\}  ].
    least-upper-bound(\{ac:fset(fset(T))|  \muparrow{}fset-antichain(eq;ac)\}  ;ac1,ac2.fset-ac-le(eq;ac1;ac2);
                                        ac1;ac2;fset-ac-lub(eq;ac1;ac2))



Date html generated: 2016_05_14-PM-03_48_54
Last ObjectModification: 2016_01_14-PM-10_40_36

Theory : finite!sets


Home Index