forall_mem_inter_of_forall_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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