Pairwise

📁 Source: Mathlib/Data/List/Pairwise.lean

Statistics

Metric	Count
Definitions	0
Theorems cons_cons_of_trans, decide, forall, forall_of_forall, head!_le, of_reverse, pwFilter, rel_dropLast_getLast, rel_getLast, rel_getLast_of_rel_getLast_getLast, rel_get_of_le, rel_get_of_lt, rel_head, rel_head_of_rel_head_head, rel_head_tail, reverse, set_pairwise, cons, decide, head!_le, le_head!, rel_get_of_le, rel_get_of_lt, pairwise_cons_cons_iff_of_trans, pairwise_iff, pairwise_of_reflexive_of_forall_ne, pairwise_replicate_of_refl, sorted_cons_cons, sorted_replicate	29
Total	29

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
pairwise_cons_cons_iff_of_trans 📖	—	—	—	—	—
pairwise_iff 📖	—	—	—	—	—
pairwise_of_reflexive_of_forall_ne 📖	—	Reflexive	—	—	—
pairwise_replicate_of_refl 📖	—	—	—	—	refl_of
sorted_cons_cons 📖	—	—	—	—	pairwise_cons_cons_iff_of_trans
sorted_replicate 📖	—	—	—	—	pairwise_replicate_of_refl

List.Pairwise

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cons_cons_of_trans 📖	—	—	—	—	—
decide 📖	—	—	—	—	—
forall 📖	—	Symmetric	—	—	forall_of_forall
forall_of_forall 📖	—	Symmetric	—	—	Symmetric.flip_eq
head!_le 📖	—	—	—	—	refl_of
of_reverse 📖	—	—	—	—	—
pwFilter 📖	—	—	—	—	—
rel_dropLast_getLast 📖	—	—	—	—	rel_head_tail
rel_getLast 📖	—	—	—	—	rel_getLast_of_rel_getLast_getLast refl_of
rel_getLast_of_rel_getLast_getLast 📖	—	—	—	—	rel_dropLast_getLast
rel_get_of_le 📖	—	—	—	—	refl
rel_get_of_lt 📖	—	—	—	—	—
rel_head 📖	—	—	—	—	rel_head_of_rel_head_head refl_of
rel_head_of_rel_head_head 📖	—	—	—	—	—
rel_head_tail 📖	—	—	—	—	—
reverse 📖	—	—	—	—	—
set_pairwise 📖	mathematical	Symmetric	Set.Pairwise setOf	—	forall

List.Sorted

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cons 📖	—	—	—	—	List.Pairwise.cons_cons_of_trans
decide 📖	—	—	—	—	List.Pairwise.decide
head!_le 📖	—	—	—	—	List.Pairwise.head!_le
le_head! 📖	—	—	—	—	List.Pairwise.head!_le
rel_get_of_le 📖	—	—	—	—	List.Pairwise.rel_get_of_le
rel_get_of_lt 📖	—	—	—	—	List.Pairwise.rel_get_of_lt

---

← Back to Index