### Nuprl Lemma : ni-eventually-equal-equiv

EquivRel(ℕ∞;f,g.ni-eventually-equal(f;g))

Proof

Definitions occuring in Statement :  ni-eventually-equal: ni-eventually-equal(f;g) nat-inf: ℕ∞ equiv_rel: EquivRel(T;x,y.E[x; y])
Definitions unfolded in proof :  equiv_rel: EquivRel(T;x,y.E[x; y]) trans: Trans(T;x,y.E[x; y]) sym: Sym(T;x,y.E[x; y]) refl: Refl(T;x,y.E[x; y]) and: P ∧ Q cand: c∧ B all: x:A. B[x] ni-eventually-equal: ni-eventually-equal(f;g) member: t ∈ T implies:  Q uall: [x:A]. B[x] prop: exists: x:A. B[x] nat: le: A ≤ B less_than': less_than'(a;b) not: ¬A false: False nat-inf: ℕ∞ int_upper: {i...} decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) subtype_rel: A ⊆B guard: {T} sq_stable: SqStable(P) squash: T ge: i ≥  true: True iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  nat-inf_wf ni-eventually-equal_wf istype-void istype-le int_upper_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf istype-int 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-int_upper bool_wf upper_subtype_nat sq_stable__le equal_wf squash_wf true_wf istype-universe nat_properties subtype_rel_self iff_weakening_equal imax_wf imax_nat intformeq_wf int_formula_prop_eq_lemma int_upper_subtype_int_upper imax_ub int_upper_subtype_nat
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut lambdaFormation_alt universeIsType introduction extract_by_obid hypothesis independent_pairFormation sqequalHypSubstitution sqequalRule isectElimination thin hypothesisEquality inhabitedIsType because_Cache dependent_pairFormation_alt dependent_set_memberEquality_alt natural_numberEquality voidElimination applyEquality setElimination rename dependent_functionElimination unionElimination independent_isectElimination approximateComputation independent_functionElimination lambdaEquality_alt int_eqEquality Error :memTop,  functionIsType equalityIstype imageMemberEquality baseClosed imageElimination productElimination equalityTransitivity equalitySymmetry instantiate universeEquality applyLambdaEquality inrFormation_alt inlFormation_alt

Latex:
EquivRel(\mBbbN{}\minfty{};f,g.ni-eventually-equal(f;g))

Date html generated: 2020_05_20-AM-07_47_53
Last ObjectModification: 2019_12_31-PM-06_32_16

Theory : basic

Home Index