forall_mem_union — Mathlib

English

For any predicate p, p holds for all elements of S ∪ T if and only if p holds for all elements of S and for all elements of T.

Русский

Для любого предиката p выполняется: p(a) для всех a ∈ S ∪ T тогда и только тогда, когда p(a) выполняется для всех a ∈ S и для всех a ∈ T.

LaTeX

$$$ (\forall a, a \in s \cup t \Rightarrow p(a)) \iff (\forall a, a \in s \Rightarrow p(a)) \land (\forall a, a \in t \Rightarrow p(a)) $$$

Lean4

theorem forall_mem_union {p : α → Prop} : (∀ a ∈ s ∪ t, p a) ↔ (∀ a ∈ s, p a) ∧ ∀ a ∈ t, p a := by grind

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