English
If a ∉ s, then pairwise relations on the cons-extended index stage relate to pairwise relations on s.
Русский
Если a ∉ s, то пары-отношения в конструкторе cons соответствуют парам на s.
LaTeX
$$$\\text{Pairwise} (r\\ on\\ fun a : s.cons a ha => f a) \\iff (\\text{Pairwise} (r\\ on\\ fun a : s => f a) \\,\\wedge\\, \\forall b\\in s,\; r(f a)(f b) \\wedge r(f b)(f a)).$$$
Lean4
theorem pairwise_cons' {a : α} (ha : a ∉ s) (r : β → β → Prop) (f : α → β) :
Pairwise (r on fun a : s.cons a ha => f a) ↔
Pairwise (r on fun a : s => f a) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a) :=
by
simp only [pairwise_subtype_iff_pairwise_finset', Finset.coe_cons, Set.pairwise_insert]
grind
