sublistForall₂_map_left_iff — Mathlib

English

Mapping the left side of a Forall₂ relation through a function f preserves the Forall₂ relation on the mapped lists.

Русский

Отображение по левой стороне отношения Forall₂ через функцию f сохраняет отношение Forall₂ между отображёнными списками.

LaTeX

$$$$\\text{MapLeftForall2: } SublistForall₂\\ R\\ (\\mathrm{map}\\ f\\ l_1)\\ l_2 \\iff SublistForall₂\\ (\\lambda c b. R (f c) b)\\ l_1\\ l_2 $$$$

Lean4

@[simp]
theorem sublistForall₂_map_left_iff {f : γ → α} {l₁ : List γ} {l₂ : List β} :
    SublistForall₂ R (map f l₁) l₂ ↔ SublistForall₂ (fun c b => R (f c) b) l₁ l₂ := by simp [sublistForall₂_iff]

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