exists_mem_insert — Mathlib

English

There exists an element in insert a s satisfying P, which is either a itself or some x ∈ s with P x.

Русский

Существует элемент во вставке insert a s, удовлетворяющий P, который либо a, либо некоторый x ∈ s с P x.

LaTeX

$$$(\exists x \in \operatorname{insert} a s, P x) \iff (P a \lor \exists x \in s, P x)$$$

Lean4

theorem exists_mem_insert {P : α → Prop} {a : α} {s : Set α} : (∃ x ∈ insert a s, P x) ↔ (P a ∨ ∃ x ∈ s, P x) := by
  grind

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