mathlib
bb289539 - feat(data/list/forall2): add `list.forall₂_iff_nth_le` (#16073)

Commit
3 years ago
feat(data/list/forall2): add `list.forall₂_iff_nth_le` (#16073) Characterization of `list.forall₂` with respect to `list.nth_le` on all positions. Co-authored-by: madvorak <dvorakmartinbridge@seznam.cz> Co-authored-by: Martin Dvořák <dvorakmartinbridge@seznam.cz> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
Parents
Loading