Nuprl Lemma : rless_irreflexivity

[e:ℝ]. False supposing e < e


Proof




Definitions occuring in Statement :  rless: x < y real: uimplies: supposing a uall: [x:A]. B[x] false: False
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a false: False rless: x < y sq_exists: x:{A| B[x]} nat_plus: + less_than: a < b squash: T and: P ∧ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] implies:  Q not: ¬A all: x:A. B[x] top: Top prop:
Lemmas referenced :  real_wf rless_wf int_formula_prop_wf int_term_value_constant_lemma int_term_value_var_lemma int_term_value_add_lemma int_formula_prop_less_lemma itermConstant_wf itermVar_wf itermAdd_wf intformless_wf satisfiable-full-omega-tt nat_plus_properties
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution setElimination thin rename lemma_by_obid isectElimination hypothesisEquality hypothesis imageElimination productElimination natural_numberEquality independent_isectElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality sqequalRule computeAll because_Cache equalityTransitivity equalitySymmetry

Latex:
\mforall{}[e:\mBbbR{}].  False  supposing  e  <  e



Date html generated: 2016_05_18-AM-07_10_00
Last ObjectModification: 2016_01_17-AM-01_50_55

Theory : reals


Home Index