English
The family antidiagonalTuple k n is pairwise with respect to the Pi.Lex order: any two distinct elements are ordered by Pi.Lex.
Русский
Для antidiagonalTuple k n выполняется попарное отношение Pi.Lex: любые две различные элементы упорядочены по Pi.Lex.
LaTeX
$$$ (antidiagonalTuple k n).Pairwise (Pi.Lex (·<·) @fun _ => (·<·)) $$$
Lean4
theorem antidiagonalTuple_pairwise_pi_lex : ∀ k n, (antidiagonalTuple k n).Pairwise (Pi.Lex (· < ·) @fun _ => (· < ·))
| 0, 0 => List.pairwise_singleton _ _
| 0, _ + 1 => List.Pairwise.nil
| k + 1, n =>
by
simp_rw [antidiagonalTuple, List.pairwise_flatMap, List.pairwise_map, List.mem_map, forall_exists_index, and_imp,
forall_apply_eq_imp_iff₂]
simp only [mem_antidiagonal, Prod.forall]
simp only [Fin.pi_lex_lt_cons_cons, true_and, lt_self_iff_false, false_or]
refine ⟨fun _ _ _ => antidiagonalTuple_pairwise_pi_lex k _, ?_⟩
induction n with
| zero =>
rw [antidiagonal_zero]
exact List.pairwise_singleton _ _
| succ n n_ih =>
rw [antidiagonal_succ, List.pairwise_cons, List.pairwise_map]
refine ⟨fun p hp x hx y hy => ?_, ?_⟩
· rw [List.mem_map, Prod.exists] at hp
obtain ⟨a, b, _, rfl : (Nat.succ a, b) = p⟩ := hp
exact Or.inl (Nat.zero_lt_succ _)
dsimp
simp_rw [Nat.succ_inj, Nat.succ_lt_succ_iff]
exact n_ih
