Nuprl Lemma : constrained-antichain-lattice_wf

[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:fset(T) ⟶ 𝔹].
  constrained-antichain-lattice(T;eq;P) ∈ BoundedDistributiveLattice 
  supposing (∀x,y:fset(T).  (y ⊆  (↑(P x))  (↑(P y)))) ∧ (↑(P {}))


Proof




Definitions occuring in Statement :  constrained-antichain-lattice: constrained-antichain-lattice(T;eq;P) bdd-distributive-lattice: BoundedDistributiveLattice empty-fset: {} f-subset: xs ⊆ ys fset: fset(T) deq: EqDecider(T) assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] implies:  Q and: P ∧ Q member: t ∈ T apply: a function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a and: P ∧ Q constrained-antichain-lattice: constrained-antichain-lattice(T;eq;P) prop: so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] cand: c∧ B assert: b ifthenelse: if then else fi  fset-antichain: fset-antichain(eq;ac) fset-pairwise: fset-pairwise(x,y.R[x; y];s) fset-null: fset-null(s) null: null(as) fset-filter: {x ∈ P[x]} filter: filter(P;l) reduce: reduce(f;k;as) list_ind: list_ind empty-fset: {} nil: [] it: btrue: tt true: True fset-all: fset-all(s;x.P[x]) so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] least-upper-bound: least-upper-bound(T;x,y.R[x; y];a;b;c) fset-ac-le: fset-ac-le(eq;ac1;ac2) subtype_rel: A ⊆B implies:  Q greatest-lower-bound: greatest-lower-bound(T;x,y.R[x; y];a;b;c) iff: ⇐⇒ Q rev_implies:  Q squash: T guard: {T} uiff: uiff(P;Q) top: Top
Lemmas referenced :  mk-bounded-distributive-lattice-from-order fset_wf assert_wf fset-antichain_wf fset-all_wf fset-constrained-ac-glb_wf fset-constrained-ac-lub_wf empty-fset_wf fset-ac-le_wf fset-ac-order-constrained assert_witness fset-null_wf fset-filter_wf bnot_wf deq-f-subset_wf set_wf fset-ac-le-singleton-empty bool_wf all_wf iff_wf f-subset_wf equal_wf squash_wf true_wf fset-ac-le-distributive-constrained iff_weakening_equal deq_wf fset-singleton_wf fset-antichain-singleton fset-all-iff deq-fset_wf member-fset-singleton fset-member_wf fset-constrained-ac-lub-is-lub fset-constrained-ac-glb-is-glb empty-fset-ac-le
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin extract_by_obid isectElimination setEquality cumulativity hypothesisEquality hypothesis productEquality sqequalRule lambdaEquality applyEquality functionExtensionality lambdaFormation setElimination rename because_Cache dependent_set_memberEquality natural_numberEquality independent_pairFormation independent_isectElimination dependent_functionElimination independent_pairEquality independent_functionElimination isect_memberEquality instantiate equalityTransitivity equalitySymmetry functionEquality imageElimination imageMemberEquality baseClosed universeEquality axiomEquality hyp_replacement applyLambdaEquality voidElimination voidEquality

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[P:fset(T)  {}\mrightarrow{}  \mBbbB{}].
    constrained-antichain-lattice(T;eq;P)  \mmember{}  BoundedDistributiveLattice 
    supposing  (\mforall{}x,y:fset(T).    (y  \msubseteq{}  x  {}\mRightarrow{}  (\muparrow{}(P  x))  {}\mRightarrow{}  (\muparrow{}(P  y))))  \mwedge{}  (\muparrow{}(P  \{\}))



Date html generated: 2017_10_05-AM-00_36_42
Last ObjectModification: 2017_07_28-AM-09_15_09

Theory : lattices


Home Index