Nuprl Lemma : dM-lift-nc-0

J:fset(ℕ). ∀j:{i:ℕ| ¬i ∈ J} . ∀v:Point(dM(J)).  ((dM-lift(J;J+j;(j0)) v) v ∈ Point(dM(J)))


Proof




Definitions occuring in Statement :  nc-0: (i0) add-name: I+i dM-lift: dM-lift(I;J;f) dM: dM(I) fset-member: a ∈ s fset: fset(T) int-deq: IntDeq nat: all: x:A. B[x] not: ¬A set: {x:A| B[x]}  apply: a equal: t ∈ T lattice-point: Point(l)
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] subtype_rel: A ⊆B DeMorgan-algebra: DeMorganAlgebra so_lambda: λ2x.t[x] prop: and: P ∧ Q guard: {T} uimplies: supposing a so_apply: x[s] not: ¬A implies:  Q nat: false: False ge: i ≥  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] nc-0: (i0) names: names(I) bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff sq_type: SQType(T) bnot: ¬bb assert: b true: True squash: T iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  lattice-point_wf dM_wf subtype_rel_set DeMorgan-algebra-structure_wf lattice-structure_wf lattice-axioms_wf bounded-lattice-structure-subtype DeMorgan-algebra-structure-subtype subtype_rel_transitivity bounded-lattice-structure_wf bounded-lattice-axioms_wf equal_wf lattice-meet_wf lattice-join_wf DeMorgan-algebra-axioms_wf istype-nat fset-member_wf nat_wf int-deq_wf strong-subtype-deq-subtype strong-subtype-set3 le_wf istype-int strong-subtype-self istype-void fset_wf f-subset-add-name add-name_wf nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf istype-le f-subset_wf nc-0_wf eq_int_wf eqtt_to_assert assert_of_eq_int eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot neg_assert_of_eq_int dM_inc_wf names_wf squash_wf true_wf istype-universe dM-lift-is-id subtype_rel_self iff_weakening_equal int_subtype_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt universeIsType cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality sqequalRule instantiate lambdaEquality_alt productEquality cumulativity because_Cache independent_isectElimination isectEquality setIsType functionIsType intEquality natural_numberEquality dependent_functionElimination setElimination rename dependent_set_memberEquality_alt unionElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality Error :memTop,  independent_pairFormation voidElimination inhabitedIsType equalityElimination equalityTransitivity equalitySymmetry productElimination equalityIstype promote_hyp imageElimination universeEquality imageMemberEquality baseClosed

Latex:
\mforall{}J:fset(\mBbbN{}).  \mforall{}j:\{i:\mBbbN{}|  \mneg{}i  \mmember{}  J\}  .  \mforall{}v:Point(dM(J)).    ((dM-lift(J;J+j;(j0))  v)  =  v)



Date html generated: 2020_05_20-PM-01_36_33
Last ObjectModification: 2020_01_06-PM-00_03_37

Theory : cubical!type!theory


Home Index