Nuprl Lemma : rmax-idempotent

[x:ℝ]. (rmax(x;x) x)


Proof




Definitions occuring in Statement :  rmax: rmax(x;y) req: y real: uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T and: P ∧ Q cand: c∧ B uiff: uiff(P;Q) uimplies: supposing a implies:  Q
Lemmas referenced :  rmax_lb rleq_weakening_equal rleq-rmax rleq_antisymmetry req_witness rmax_wf real_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin because_Cache productElimination independent_isectElimination hypothesis independent_pairFormation hypothesisEquality independent_functionElimination

Latex:
\mforall{}[x:\mBbbR{}].  (rmax(x;x)  =  x)



Date html generated: 2016_05_18-AM-07_19_53
Last ObjectModification: 2015_12_28-AM-00_46_50

Theory : reals


Home Index