pairwise_fin_succ_iff — Mathlib

English

For a relation R on Fin n.succ, Pairwise R is equivalent to R certain boundary checks and a reduced pairwise on successors.

Русский

Для отношения R на Fin n.succ попарность равна сумме крайних условий и попарности на successors.

LaTeX

$$$\\operatorname{Pairwise}(R) \\iff \\bigl(\\forall i\\in Fin\\, n, R(i.succ,0)\\bigr) \\land \\bigl(\\forall j\\in Fin\\, R(0,j.succ)\\bigr) \\land \\operatorname{Pairwise}(\\lambda i j. R(i.succ, j.succ))$$$

Lean4

theorem pairwise_fin_succ_iff {n : ℕ} {R : Fin n.succ → Fin n.succ → Prop} :
    Pairwise R ↔ (∀ i, R (Fin.succ i) 0) ∧ (∀ j, R 0 (Fin.succ j)) ∧ Pairwise fun i j => R (Fin.succ i) (Fin.succ j)
    where
  mp
    h :=
    ⟨fun _ => h (Fin.succ_ne_zero _), fun _ => h (Fin.succ_ne_zero _).symm, fun _i _j hij =>
      h <| Fin.succ_inj.not.2 hij⟩
  mpr
    | ⟨hi, hj, h⟩ =>
      Fin.cases (Fin.cases nofun fun j _ => hj j)
        (fun i => Fin.cases (fun _ => hi i) fun _j hij => h (ne_of_apply_ne _ hij))

Похожие утверждения