forall_mem_union — Mathlib

English

For any predicate p, (for all x ∈ l1 ∪ l2, p x) is equivalent to ((for all x ∈ l1, p x) and (for all x ∈ l2, p x)).

Русский

Для любого предиката p верно: для всех x в l1 ∪ l2 выполняется p x эквивалентно (для всех x в l1, p x) и (для всех x в l2, p x).

LaTeX

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

Lean4

theorem forall_mem_union : (∀ x ∈ l₁ ∪ l₂, p x) ↔ (∀ x ∈ l₁, p x) ∧ ∀ x ∈ l₂, p x := by
  simp only [mem_union_iff, or_imp, forall_and]

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