pairwise_fin_succ_iff_of_isSymm — Mathlib

English

If R is symmetric, Pairwise R on Fin n.succ is equivalent to R 0 with succ j and Pairwise on succ-succ.

Русский

Если R симметрично, то попарность R на Fin n.succ эквивалентна R(0, succ j) и попарности на парах (succ i, succ j).

LaTeX

$$$\\text{IsSymm } R \\Rightarrow \\operatorname{Pairwise}(R) \\iff (\\forall j, R(0, j \\text{ .succ})) \\land \\operatorname{Pairwise}(\\lambda i j. R(i. succ, j. succ))$$$

Lean4

theorem pairwise_fin_succ_iff_of_isSymm {n : ℕ} {R : Fin n.succ → Fin n.succ → Prop} [IsSymm _ R] :
    Pairwise R ↔ (∀ j, R 0 (Fin.succ j)) ∧ Pairwise fun i j => R (Fin.succ i) (Fin.succ j) := by
  simp only [pairwise_fin_succ_iff, comm (b := 0) (r := R), and_self_left]

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