forall_mem_of_forall_mem_union_left

Mathlib.Data.List.Lattice

URI: https://scilib.ai/kg/mathlib#List.forall_mem_of_forall_mem_union_left

English

If all elements of l1 ∪ l2 satisfy p, then all elements of l1 satisfy p.

Русский

Если все элементы l1 ∪ l2 удовлетворяют p, то все элементы l1 удовлетворяют p.

LaTeX

$$$$ (\\forall x \\in l_1 \\cup l_2, p x) \\Rightarrow (\\forall x \\in l_1, p x). $$$$

Lean4

theorem forall_mem_of_forall_mem_union_left (h : ∀ x ∈ l₁ ∪ l₂, p x) : ∀ x ∈ l₁, p x :=
  (forall_mem_union.1 h).1

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru