sublistForall₂ — Mathlib

English

If l1 is a sublist of l2 and Rₐ is reflexive, then there is a relation that every corresponding pair from l1 to l2 satisfies via SublistForall₂.

Русский

Если l1 является подсписком l2, и Rₐ рефлексивно, то существует отношение, при котором каждая соответствующая пара элементов от l1 к l2 удовлетворяет via SublistForall₂.

LaTeX

$$$\forall {\alpha}, {R_\alpha}, {l_1 l_2:\ List\;\alpha},\; l_1 <+ l_2 \Rightarrow [IsRefl]\alpha\; R_\alpha \;:\; \text{SublistForall₂ } R_\alpha l_1 l_2$$$

Lean4

theorem sublistForall₂ {l₁ l₂ : List α} (h : l₁ <+ l₂) [IsRefl α Rₐ] : SublistForall₂ Rₐ l₁ l₂ :=
  sublistForall₂_iff.2 ⟨l₁, forall₂_refl l₁, h⟩

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