rel_append — Mathlib

English

If two relations hold for corresponding pieces, concatenating lists preserves the relation (Forall₂ with ++).

Русский

Если для соответствующих частей выполняются отношения, конкатенация списков сохраняет отношение (Forall₂ с ++).

LaTeX

$$$ \text{rel\_append} : (Forall₂\ R \Rightarrow Forall₂\ R \Rightarrow Forall₂\ R)\ (\cdot \;++\;\cdot)\ (\cdot \;++\;\cdot)$$$

Lean4

theorem rel_append : (Forall₂ R ⇒ Forall₂ R ⇒ Forall₂ R) (· ++ ·) (· ++ ·)
  | [], [], _, _, _, hl => hl
  | _, _, Forall₂.cons h₁ h₂, _, _, hl => Forall₂.cons h₁ (rel_append h₂ hl)

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