Commit 2023-08-29 03:36 d7b5d387

View on Github →

feat: lower bounds for Levenshtein edit distance (#6118)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/EditDistance/Bounds.lean

added theorem le_levenshtein_append

added theorem le_levenshtein_cons

added theorem le_suffixLevenshtein_append_minimum

added theorem le_suffixLevenshtein_cons_minimum

added theorem suffixLevenshtein_minimum_le_levenshtein_append

added theorem suffixLevenshtein_minimum_le_levenshtein_cons

Modified Mathlib/Data/List/MinMax.lean

added theorem List.le_minimum_of_forall_le

deleted theorem List.le_minimum_of_mem'

added theorem List.maximum_le_of_forall_le

added theorem List.minimum_le_of_mem'