forall — Mathlib

English

If a relation r is symmetric and a finite multiset s is pairwise related by r, then for any a ∈ s and b ∈ s with a ≠ b, we have r a b.

Русский

Если отношение r симметрично и множество s попарно связано отношением r, то для любых элементов a,b из s с a ≠ b верно r a b.

LaTeX

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

Lean4

theorem «forall» (H : Symmetric r) (hs : Pairwise r s) : ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → a ≠ b → r a b :=
  let ⟨_, hl₁, hl₂⟩ := hs
  hl₁.symm ▸ hl₂.forall H

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