Commit 2023-01-10 14:58 8749fdcc

View on Github →

feat port: Data.List.Pairwise (#1450)

Estimated changes

Modified Mathlib/Data/List/Pairwise.lean

added theorem List.Pairwise.and

added theorem List.Pairwise.drop

added theorem List.Pairwise.filter

added theorem List.Pairwise.filter_map

added theorem List.Pairwise.forall

added theorem List.Pairwise.forall_of_forall

added theorem List.Pairwise.forall_of_forall_of_flip

added theorem List.Pairwise.iff

added theorem List.Pairwise.imp_mem

added theorem List.Pairwise.imp₂

added theorem List.Pairwise.of_cons

added theorem List.Pairwise.pmap

added theorem List.Pairwise.set_pairwise

added theorem List.Pairwise.tail

added theorem List.forall_mem_pwFilter

added theorem List.pairwise_and_iff

added theorem List.pairwise_bind

added theorem List.pairwise_filter

added theorem List.pairwise_filterMap

added theorem List.pairwise_iff_get

added theorem List.pairwise_iff_nthLe

added theorem List.pairwise_join

added theorem List.pairwise_map'

added theorem List.pairwise_of_forall

added theorem List.pairwise_of_forall_mem_list

added theorem List.pairwise_of_reflexive_of_forall_ne

added theorem List.pairwise_of_reflexive_on_dupl_of_forall_ne

added theorem List.pairwise_pair

added theorem List.pairwise_pmap

added theorem List.pairwise_pwFilter

added theorem List.pairwise_repeat

added theorem List.pairwise_replicate

added theorem List.pwFilter_cons_of_neg

added theorem List.pwFilter_cons_of_pos

added theorem List.pwFilter_eq_self

added theorem List.pwFilter_idempotent

added theorem List.pwFilter_map

added theorem List.pwFilter_nil

added theorem List.pwFilter_sublist

added theorem List.pwFilter_subset