Commit 2023-01-10 17:03 7ca728c9

View on Github →

feat: port Data.List.Chain (#1451)

Estimated changes

Modified Mathlib/Data/List/Chain.lean

added theorem List.Chain'.append

added theorem List.Chain'.append_overlap

added theorem List.Chain'.cons'

added theorem List.Chain'.cons

added theorem List.Chain'.drop

added theorem List.Chain'.iff

added theorem List.Chain'.iff_mem

added theorem List.Chain'.imp

added theorem List.Chain'.imp_head

added theorem List.Chain'.infix

added theorem List.Chain'.init

added theorem List.Chain'.left_of_append

added theorem List.Chain'.prefix

added theorem List.Chain'.rel_head

added theorem List.Chain'.rel_head?

added theorem List.Chain'.right_of_append

added theorem List.Chain'.suffix

added theorem List.Chain'.tail

added theorem List.Chain'.take

added theorem List.Chain.iff

added theorem List.Chain.iff_mem

added theorem List.Chain.induction

added theorem List.Chain.induction_head

added theorem List.Pairwise.chain'

added theorem List.chain'_append

added theorem List.chain'_append_cons_cons

added theorem List.chain'_cons'

added theorem List.chain'_cons

added theorem List.chain'_iff_get

added theorem List.chain'_iff_nthLe

added theorem List.chain'_iff_pairwise

added theorem List.chain'_isInfix

added theorem List.chain'_map

added theorem List.chain'_map_of_chain'

added theorem List.chain'_nil

added theorem List.chain'_of_chain'_map

added theorem List.chain'_pair

added theorem List.chain'_reverse

added theorem List.chain'_singleton

added theorem List.chain'_split

added theorem List.chain_append_cons_cons

added theorem List.chain_append_singleton_iff_forall₂

added theorem List.chain_iff_forall₂

added theorem List.chain_iff_get

added theorem List.chain_iff_nthLe

modified theorem List.chain_iff_pairwise

added theorem List.chain_map

added theorem List.chain_map_of_chain

added theorem List.chain_of_chain_cons

added theorem List.chain_of_chain_map

added theorem List.chain_of_chain_pmap

added theorem List.chain_pmap_of_chain

added theorem List.chain_singleton

added theorem List.chain_split

added theorem List.exists_chain_of_relationReflTransGen

added theorem List.rel_of_chain_cons

added theorem List.relationReflTransGen_of_exists_chain