Commit 2024-06-06 21:05 f6837cfe

View on Github →

refactor: reduceOption_length_le (#11671) Reproves reduceOption_length_eq_iff and reduceOption_length_le with new auxiliary lemmas - primarily length_eq_reduceOption_length_add_filter_none.

Estimated changes

Modified Mathlib/Data/List/Basic.lean

added theorem List.length_eq_length_filter_add

Modified Mathlib/Data/List/ReduceOption.lean

added theorem List.length_eq_reduceOption_length_add_filter_none

added theorem List.reduceOption_length_eq

Modified Mathlib/Data/Option/Basic.lean

added theorem Option.bnot_comp_isNone

added theorem Option.bnot_comp_isSome

added theorem Option.bnot_isNone

added theorem Option.bnot_isSome

added theorem Option.isNone_eq_false_iff