Nuprl Lemma : std-simplex-void

[n:ℤ]. ¬Δ(n) supposing n < 0


Proof




Definitions occuring in Statement :  std-simplex: Δ(n) less_than: a < b uimplies: supposing a uall: [x:A]. B[x] not: ¬A natural_number: $n int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a not: ¬A implies:  Q false: False std-simplex: Δ(n) and: P ∧ Q so_lambda: λ2x.t[x] top: Top so_apply: x[s] uiff: uiff(P;Q) sq_type: SQType(T) all: x:A. B[x] guard: {T} true: True
Lemmas referenced :  std-simplex_wf istype-less_than istype-int rsum-empty istype-void req-int subtype_base_sq int_subtype_base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut lambdaFormation_alt thin sqequalHypSubstitution setElimination rename productElimination hypothesis because_Cache independent_functionElimination voidElimination universeIsType extract_by_obid isectElimination hypothesisEquality sqequalRule lambdaEquality_alt dependent_functionElimination functionIsTypeImplies inhabitedIsType natural_numberEquality isect_memberEquality_alt isectIsTypeImplies independent_isectElimination instantiate cumulativity intEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[n:\mBbbZ{}].  \mneg{}\mDelta{}(n)  supposing  n  <  0



Date html generated: 2019_10_30-AM-11_30_29
Last ObjectModification: 2019_07_31-PM-02_48_41

Theory : real!vectors


Home Index