English
Let s be a finite subset of a partially ordered set ι. The off-diagonal pairs from s that satisfy the first coordinate is less than the second are exactly those with the first coordinate less than or equal to the second, since for any off-diagonal pair we have i ≠ j, hence i < j if and only if i ≤ j.
Русский
Пусть s — конечное подмножество частично упорядоченного множества ι. Множество попарных элементов вне диагонали из s, удовлетворяющих i1 < i2, совпадает с множеством таких же пар, удовлетворяющих i1 ≤ i2, поскольку для любой пары с i ≠ j верно, что i < j тогда и только тогда, когда i ≤ j.
LaTeX
$$$$ s.offDiag.filter(\lambda i:\, i.1 < i.2) = s.offDiag.filter(\lambda i:\, i.1 \le i.2). $$$$
Lean4
theorem offDiag_filter_lt_eq_filter_le {ι} [PartialOrder ι] [DecidableEq ι] [DecidableLE ι] [DecidableLT ι]
(s : Finset ι) : s.offDiag.filter (fun i => i.1 < i.2) = s.offDiag.filter (fun i => i.1 ≤ i.2) :=
by
rw [Finset.filter_inj']
rintro ⟨i, j⟩
simp_rw [mem_offDiag, and_imp]
rintro _ _ h
rw [Ne.le_iff_lt h]
