Nuprl Lemma : sq_stable__ss-mem-basic
∀[X:SeparationSpace]. ∀B:ss-basic(X). ∀x:Point(X). SqStable(x ∈ B)
Proof
Definitions occuring in Statement :
ss-mem-basic: x ∈ B,
ss-basic: ss-basic(X),
ss-point: Point(ss),
separation-space: SeparationSpace,
sq_stable: SqStable(P),
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
sq_stable: SqStable(P),
implies: P ⇒ Q,
ss-mem-basic: x ∈ B,
member: t ∈ T,
l_all: (∀x∈L.P[x]),
ss-basic: ss-basic(X),
uimplies: b supposing a,
guard: {T},
int_seg: {i..j-},
lelt: i ≤ j < k,
and: P ∧ Q,
decidable: Dec(P),
or: P ∨ Q,
not: ¬A,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
false: False,
top: Top,
prop: ℙ,
less_than: a < b,
squash: ↓T,
subtype_rel: A ⊆r B,
rless: x < y,
sq_exists: ∃x:A [B[x]],
ss-ap: f(x),
ss-point: Point(ss),
record-select: r.x,
real-ss: ℝ,
mk-ss: Point=P #=Sep cotrans=C,
record-update: r[x := v],
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
bfalse: ff,
btrue: tt,
real: ℝ,
iff: P ⇐⇒ Q
Lemmas referenced :
select_wf,
int_seg_properties,
decidable__le,
full-omega-unsat,
intformand_wf,
intformnot_wf,
intformle_wf,
itermConstant_wf,
itermVar_wf,
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,
decidable__lt,
intformless_wf,
int_formula_prop_less_lemma,
rlessw_wf,
subtype_rel_self,
rless_wf,
ss-ap_wf,
real-ss_wf,
equal_wf,
int_seg_wf,
length_wf,
ss-point_wf,
ss-fun_wf,
real_wf,
squash_wf,
ss-mem-basic_wf,
ss-basic_wf,
separation-space_wf,
ss-fun-point,
iff_weakening_equal
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
introduction,
sqequalHypSubstitution,
lambdaEquality,
spreadEquality,
cut,
extract_by_obid,
isectElimination,
thin,
because_Cache,
independent_isectElimination,
hypothesisEquality,
hypothesis,
setElimination,
rename,
productElimination,
dependent_functionElimination,
unionElimination,
natural_numberEquality,
approximateComputation,
independent_functionElimination,
dependent_pairFormation,
int_eqEquality,
intEquality,
isect_memberEquality,
voidElimination,
voidEquality,
sqequalRule,
independent_pairFormation,
imageElimination,
applyEquality,
equalityTransitivity,
equalitySymmetry,
productEquality,
dependent_set_memberEquality
Latex:
\mforall{}[X:SeparationSpace]. \mforall{}B:ss-basic(X). \mforall{}x:Point(X). SqStable(x \mmember{} B)
Date html generated:
2020_05_20-PM-01_21_54
Last ObjectModification:
2018_07_06-PM-04_40_43
Theory : intuitionistic!topology
Home
Index