forall_mem_inter_of_forall_left — Mathlib

English

If p(x) holds for all x in l1, then for any l2 and any x ∈ l1 ∩ l2, p(x) holds.

Русский

Если для всех x из l1 верно p(x), то для любого x ∈ l1 ∩ l2 верно p(x).

LaTeX

$$$\\forall {\\\\alpha} {l_1 : List \\\\alpha} {p : \\\\alpha \\\\rightarrow Prop} [DecidableEq \\\\alpha], (\\\\forall x, x \\in l_1 \\\\rightarrow p x) \\\\rightarrow \\\\forall (l_2 : List \\\\alpha) (x : \\\\alpha), x \\in l_1 \\\\cap l_2 \\\rightarrow p x$$$

Lean4

theorem forall_mem_inter_of_forall_left (h : ∀ x ∈ l₁, p x) (l₂ : List α) : ∀ x, x ∈ l₁ ∩ l₂ → p x :=
  BAll.imp_left (fun _ => mem_of_mem_inter_left) h

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