affeldt-aist / infotheo

A Coq formalization of information theory and linear error-correcting codes
GNU Lesser General Public License v2.1
64 stars 15 forks source link

add semilattconvtype and lub_absorbs_conv (the binary counterpart of biglub_hull) #34

Closed t6s closed 3 years ago

t6s commented 3 years ago

A move towards proving the lemma in altprob as suggested by Jacques