Skip to content

GitLab

I
Iris
Merged
Opened by Dan Frumin@dfrumin
Report abuse

big_sepM2 and associated lemmas

Following big_sepL2 and big_sepM. Based on some code from @robbertkrebbers.

Would like to hear your comments and also add some helpful lemmas about this big op.

Edited by Dan Frumin