set_pairwise_iff — Mathlib

English

If r is reflexive, then s.Pairwise r is equivalent to: for all a,b in s, r a b.

Русский

Если r рефлексивно, то s.Pairwise r эквивалентно: для всех a,b в s выполняется r a b.

LaTeX

$$$\\text{Reflexive}(r) \\Rightarrow (s.Pairwise r \\iff \\forall a\\in s, \\forall b\\in s, r(a,b))$$$

Lean4

theorem _root_.Reflexive.set_pairwise_iff (hr : Reflexive r) : s.Pairwise r ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → r a b :=
  forall₄_congr fun a _ _ _ => or_iff_not_imp_left.symm.trans <| or_iff_right_of_imp <| Eq.ndrec <| hr a

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