Nuprl Lemma : general-bounded-lattice-structure_wf

GeneralBoundedLatticeStructure ∈ 𝕌'


Proof




Definitions occuring in Statement :  general-bounded-lattice-structure: GeneralBoundedLatticeStructure member: t ∈ T universe: Type
Definitions unfolded in proof :  general-bounded-lattice-structure: GeneralBoundedLatticeStructure member: t ∈ T uall: [x:A]. B[x] so_lambda: λ2x.t[x] so_apply: x[s] record+: record+ record-select: r.x subtype_rel: A ⊆B eq_atom: =a y ifthenelse: if then else fi  btrue: tt guard: {T} prop:
Lemmas referenced :  record_wf top_wf record+_wf subtype_rel_self
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut lemma_by_obid sqequalHypSubstitution isectElimination thin sqequalRule lambdaEquality cumulativity hypothesis atomEquality equalityTransitivity equalitySymmetry universeEquality tokenEquality dependentIntersectionElimination applyEquality instantiate functionEquality dependentIntersectionEqElimination hypothesisEquality because_Cache

Latex:
GeneralBoundedLatticeStructure  \mmember{}  \mBbbU{}'



Date html generated: 2020_05_20-AM-08_57_45
Last ObjectModification: 2015_12_28-PM-01_54_57

Theory : lattices


Home Index