Nuprl Lemma : real-closed-interval-lattice_wf
∀[a,b:ℝ]. real-closed-interval-lattice(a;b) ∈ GeneralBoundedDistributiveLattice supposing a ≤ b
Proof
Definitions occuring in Statement :
real-closed-interval-lattice: real-closed-interval-lattice(a;b),
general-bounded-distributive-lattice: GeneralBoundedDistributiveLattice,
rleq: x ≤ y,
real: ℝ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
real-closed-interval-lattice: real-closed-interval-lattice(a;b),
all: ∀x:A. B[x],
top: Top,
and: P ∧ Q,
prop: ℙ,
so_lambda: λ2x y.t[x; y],
cand: A c∧ B,
iff: P ⇐⇒ Q,
implies: P ⇒ Q,
or: P ∨ Q,
guard: {T},
so_apply: x[s1;s2],
uiff: uiff(P;Q),
so_lambda: λ2x.t[x],
so_apply: x[s],
equiv_rel: EquivRel(T;x,y.E[x; y]),
refl: Refl(T;x,y.E[x; y]),
sym: Sym(T;x,y.E[x; y]),
trans: Trans(T;x,y.E[x; y]),
sq_stable: SqStable(P),
squash: ↓T
Lemmas referenced :
member_rccint_lemma,
mk-general-bounded-dist-lattice_wf,
real_wf,
rleq_wf,
rmin_wf,
rmin_ub,
rmin_lb,
rmax_wf,
rmax_ub,
rmax_lb,
rleq_weakening_equal,
req_wf,
rmin-com,
req_witness,
set_wf,
rmax-com,
req_inversion,
rmin-assoc,
rmax-assoc,
rmax-rmin-absorption,
rmin-rmax-absorption,
rmin-rmax-distrib,
req_weakening,
req_transitivity,
sq_stable__req,
rmin-req2,
rmax-req2,
sq_stable__rleq
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
isect_memberEquality,
voidElimination,
voidEquality,
hypothesis,
isectElimination,
setEquality,
productEquality,
hypothesisEquality,
because_Cache,
lambdaEquality,
lambdaFormation,
setElimination,
rename,
productElimination,
dependent_set_memberEquality,
independent_functionElimination,
independent_pairFormation,
independent_isectElimination,
inlFormation,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
imageMemberEquality,
baseClosed,
imageElimination
Latex:
\mforall{}[a,b:\mBbbR{}]. real-closed-interval-lattice(a;b) \mmember{} GeneralBoundedDistributiveLattice supposing a \mleq{} b
Date html generated:
2018_05_22-PM-09_56_00
Last ObjectModification:
2018_05_20-PM-10_15_13
Theory : lattices
Home
Index