Nuprl Lemma : type-incr-chain-subtype

[X:type-incr-chain{i:l}()]. ∀[n,m:ℕ].  (X n) ⊆(X m) supposing n ≤ m


Proof




Definitions occuring in Statement :  type-incr-chain: type-incr-chain{i:l}() nat: uimplies: supposing a subtype_rel: A ⊆B uall: [x:A]. B[x] le: A ≤ B apply: a
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] nat: implies:  Q false: False ge: i ≥  not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top and: P ∧ Q prop: subtype_rel: A ⊆B type-incr-chain: type-incr-chain{i:l}() decidable: Dec(P) or: P ∨ Q le: A ≤ B sq_type: SQType(T) guard: {T} sq_stable: SqStable(P) squash: T rev_uimplies: rev_uimplies(P;Q) rev_subtype_rel: A ⊇B subtract: m
Lemmas referenced :  nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf less_than_wf subtype_rel-equal decidable__le intformnot_wf itermAdd_wf int_formula_prop_not_lemma int_term_value_add_lemma le_wf add-zero subtract_wf itermSubtract_wf int_term_value_subtract_lemma subtype_base_sq int_subtype_base decidable__equal_int intformeq_wf int_formula_prop_eq_lemma nat_wf type-incr-chain_wf sq_stable__subtype_rel subtype_rel_functionality_wrt_implies subtype_rel_weakening ext-eq_inversion ext-eq_weakening minus-one-mul add-swap minus-one-mul-top add-mul-special zero-mul subtype_rel_transitivity
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename intWeakElimination natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation axiomEquality applyEquality because_Cache dependent_set_memberEquality addEquality unionElimination productElimination instantiate cumulativity equalityTransitivity equalitySymmetry functionExtensionality imageMemberEquality baseClosed imageElimination minusEquality

Latex:
\mforall{}[X:type-incr-chain\{i:l\}()].  \mforall{}[n,m:\mBbbN{}].    (X  n)  \msubseteq{}r  (X  m)  supposing  n  \mleq{}  m



Date html generated: 2018_05_21-PM-08_43_59
Last ObjectModification: 2018_05_19-PM-05_06_35

Theory : general


Home Index