Nuprl Lemma : fset-constrained-ac-lub_wf

[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:fset(T) ⟶ 𝔹]. ∀[ac1,ac2:{ac:fset(fset(T))| 
                                                             (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P a)} ].
  (lub(P;ac1;ac2) ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.P a)} )


Proof




Definitions occuring in Statement :  fset-constrained-ac-lub: lub(P;ac1;ac2) fset-antichain: fset-antichain(eq;ac) fset-all: fset-all(s;x.P[x]) fset: fset(T) deq: EqDecider(T) assert: b bool: 𝔹 uall: [x:A]. B[x] and: P ∧ Q member: t ∈ T set: {x:A| B[x]}  apply: a function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T fset-constrained-ac-lub: lub(P;ac1;ac2) and: P ∧ Q cand: c∧ B so_lambda: λ2x.t[x] so_apply: x[s] prop: all: x:A. B[x] implies:  Q sq_stable: SqStable(P) squash: T subtype_rel: A ⊆B uiff: uiff(P;Q) uimplies: supposing a fset-ac-lub: fset-ac-lub(eq;ac1;ac2) so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] iff: ⇐⇒ Q or: P ∨ Q guard: {T}
Lemmas referenced :  member-fset-union fset-union_wf f-proper-subset-dec_wf member-fset-minimals fset-member_wf assert_witness deq-fset_wf fset-all-iff equal_wf decidable__assert sq_stable_from_decidable fset-ac-lub_wf deq_wf bool_wf set_wf fset_wf fset-all_wf fset-antichain_wf assert_wf and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut setElimination thin rename sqequalRule sqequalHypSubstitution productElimination dependent_set_memberEquality because_Cache independent_pairFormation hypothesis lemma_by_obid isectElimination hypothesisEquality lambdaEquality applyEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality functionEquality universeEquality cumulativity lambdaFormation independent_functionElimination dependent_functionElimination imageMemberEquality baseClosed imageElimination independent_isectElimination unionElimination

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[P:fset(T)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[ac1,ac2:\{ac:fset(fset(T))| 
                                                                                                                          (\muparrow{}fset-antichain(eq;ac))
                                                                                                                          \mwedge{}  fset-all(ac;a.P  a)\}  ].
    (lub(P;ac1;ac2)  \mmember{}  \{ac:fset(fset(T))|  (\muparrow{}fset-antichain(eq;ac))  \mwedge{}  fset-all(ac;a.P  a)\}  )



Date html generated: 2016_05_14-PM-03_49_07
Last ObjectModification: 2016_01_14-PM-10_39_31

Theory : finite!sets


Home Index