English
If r is reflexive, then s is pairwise with respect to r iff every pair of elements of s satisfies r.
Русский
Если r рефлексивно, то s попарно по r тогда и только тогда, когда для любых a,b ∈ s выполняется r a b.
LaTeX
$$$[IsRefl \alpha r] \Rightarrow (s.Pairwise r \leftrightarrow \forall a \in s, \forall b \in s, r a b)$$$
Lean4
theorem pairwise_iff_of_refl [IsRefl α r] : s.Pairwise r ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → r a b :=
forall₄_congr fun _ _ _ _ => or_iff_not_imp_left.symm.trans <| or_iff_right_of_imp of_eq