pairwise_iff_of_refl — Mathlib

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

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