forall_mem_insert — Mathlib

English

For any a, s and predicate p, every element of insert a s satisfies p if and only if p(a) holds and every element of s satisfies p as well.

Русский

Пусть a, s и предикат p. Тогда для всех x, если x ∈ insert a s, то p(x) эквивалентно p(a) и для всех x ∈ s, p(x).

LaTeX

$$$\\bigl(\\forall x, x \\in \\operatorname{insert} a s \\rightarrow p(x)\\bigr) \\ \\iff\\ \\left(p(a) \\land \\forall x, x \\in s \\rightarrow p(x)\\right).$$$

Lean4

theorem forall_mem_insert (a : α) (s : Finset α) (p : α → Prop) :
    (∀ x, x ∈ insert a s → p x) ↔ p a ∧ ∀ x, x ∈ s → p x := by grind

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