mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

refactor: `reduceOption_length_le`

Open BoltonBailey opened this issue 1 year ago • 4 comments

Reproves reduceOption_length_eq_iff and reduceOption_length_le with new auxiliary lemmas - primarily length_eq_reduceOption_length_add_filter_none.

Open in Gitpod

BoltonBailey avatar Mar 25 '24 21:03 BoltonBailey