forall₂_same — Mathlib

English

For any list l and relation Rₐ on elements with symmetry, Forall₂ Rₐ l l holds iff every element x ∈ l satisfies Rₐ x x.

Русский

Для любого списка l и relation Rₐ на элементах, Forall₂ Rₐ l l эквивалентно тому, что каждый элемент x ∈ l удовлетворяет Rₐ x x.

LaTeX

$$$$ \\forall {l},\\text{ Forall₂ } R_\\alpha l l \\iff \\forall x \\in l,\\ R_\\alpha x x. $$$$

Lean4

@[simp]
theorem forall₂_same : ∀ {l : List α}, Forall₂ Rₐ l l ↔ ∀ x ∈ l, Rₐ x x
  | [] => by simp
  | a :: l => by simp [@forall₂_same l]

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