Nuprl Lemma : alg_le_wf

A:Type. ∀a:algebra_sig{i:l}(A).  (a.le ∈ a.car ⟶ a.car ⟶ 𝔹)


Proof




Definitions occuring in Statement :  alg_le: a.le alg_car: a.car algebra_sig: algebra_sig{i:l}(A) bool: 𝔹 all: x:A. B[x] member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T algebra_sig: algebra_sig{i:l}(A) alg_le: a.le alg_car: a.car pi1: fst(t) pi2: snd(t)
Lemmas referenced :  algebra_sig_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalHypSubstitution productElimination thin sqequalRule hypothesisEquality hypothesis lemma_by_obid dependent_functionElimination universeEquality

Latex:
\mforall{}A:Type.  \mforall{}a:algebra\_sig\{i:l\}(A).    (a.le  \mmember{}  a.car  {}\mrightarrow{}  a.car  {}\mrightarrow{}  \mBbbB{})



Date html generated: 2016_05_16-AM-07_25_58
Last ObjectModification: 2015_12_28-PM-05_08_19

Theory : algebras_1


Home Index