Nuprl Lemma : i-member_wf

[I:Interval]. ∀[x:ℝ].  (x ∈ I ∈ ℙ)


Proof




Definitions occuring in Statement :  i-member: r ∈ I interval: Interval real: uall: [x:A]. B[x] prop: member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T i-member: r ∈ I interval: Interval prop: and: P ∧ Q
Lemmas referenced :  rleq_wf rless_wf true_wf real_wf interval_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution productElimination thin unionElimination productEquality lemma_by_obid isectElimination hypothesisEquality hypothesis because_Cache axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

Latex:
\mforall{}[I:Interval].  \mforall{}[x:\mBbbR{}].    (x  \mmember{}  I  \mmember{}  \mBbbP{})



Date html generated: 2016_05_18-AM-08_19_14
Last ObjectModification: 2015_12_27-PM-11_57_48

Theory : reals


Home Index