Hi,
I am trying to prove a property in hol light regarding concatenation of
the matrices. In the proof i need a property which prove following
statement :
0 [`1 <= i`]
1 [`i <= dimindex (:N)`]
2 [`~(i' <= dimindex (:N))`]
3 [`1 <= i'`]
4 [`i' <= dimindex (:N+P)`]
`sum (1..dimindex (:M)) (\k. C$i$k * B$k$(i' - dimindex (:N))) =
(lambda j. sum (1..dimindex (:M)) (\k. C$i$k * B$k$j))$(i' - dimindex
(:N))`
Can anyone help me finding the property that proves it?
------------------------------------------------------------------------------
Mobile security can be enabling, not merely restricting. Employees who
bring their own devices (BYOD) to work are irked by the imposition of MDM
restrictions. Mobile Device Manager Plus allows you to control only the
apps on BYO-devices by containerizing them, leaving personal data untouched!
https://ad.doubleclick.net/ddm/clk/304595813;131938128;j
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
