exists_mem_insert — Mathlib

English

For any a, finite s and property p, there exists x in insert a s with p(x) if and only if p(a) holds or there exists x in s with p(x).

Русский

Для любых a, конечного s и свойства p существует элемент x в insert a s такой, что p(x), тогда и только тогда, когда p(a) выполняется или существует x в s с p(x).

LaTeX

$$$\\exists x\\, \\bigl( x \\in \\operatorname{insert} a s \\land p(x)\\bigr) \\;\\iff\\; p(a) \\lor \\exists x\\, (x \\in s \\land p(x)).$$$

Lean4

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

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