Nuprl Lemma : sq_stable__bilinear

[T:Type]. ∀[pl,tm:T ⟶ T ⟶ T].  SqStable(BiLinear(T;pl;tm))


Proof




Definitions occuring in Statement :  bilinear: BiLinear(T;pl;tm) sq_stable: SqStable(P) uall: [x:A]. B[x] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  bilinear: BiLinear(T;pl;tm) uall: [x:A]. B[x] member: t ∈ T so_lambda: λ2x.t[x] prop: and: P ∧ Q infix_ap: y so_apply: x[s] implies:  Q sq_stable: SqStable(P)
Lemmas referenced :  sq_stable__uall uall_wf equal_wf infix_ap_wf sq_stable__and sq_stable__equal squash_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaEquality cumulativity because_Cache productEquality functionExtensionality applyEquality hypothesis independent_functionElimination isect_memberEquality lambdaFormation dependent_functionElimination productElimination independent_pairEquality axiomEquality functionEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[pl,tm:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].    SqStable(BiLinear(T;pl;tm))



Date html generated: 2017_10_01-AM-08_12_54
Last ObjectModification: 2017_02_28-PM-01_57_32

Theory : gen_algebra_1


Home Index