Commit 2021-12-13 13:16 c2a9a632

View on Github →

feat(*): migrated some lemmas about disjoint lists (#126)

Estimated changes

Modified Mathlib/Data/List/Basic.lean

added def List.disjoint

added theorem List.disjoint_append_left

added theorem List.disjoint_comm

added theorem List.disjoint_cons_left

added theorem List.disjoint_iff_ne

added theorem List.disjoint_left

added theorem List.disjoint_nil_left

added theorem List.disjoint_nil_right

added theorem List.disjoint_of_disjoint_append_left_left

added theorem List.disjoint_of_disjoint_append_left_right

added theorem List.disjoint_of_disjoint_cons_left

added theorem List.disjoint_of_disjoint_cons_right

added theorem List.disjoint_of_subset_left

added theorem List.disjoint_of_subset_right

added theorem List.disjoint_right

added theorem List.disjoint_singleton

added theorem List.disjoint_symm

added theorem List.singleton_disjoint

Modified Mathlib/Data/List/Card.lean

deleted def List.disjoint

Modified Mathlib/Logic/Basic.lean

modified theorem exists_false

added theorem forall_eq'

modified theorem forall_eq