forall_mem_insert — Mathlib

English

For all x, if x ∈ insert a s then P x holds, which is equivalent to P a and for all x ∈ s, P x.

Русский

Для всех x, если x ∈ insert a s, то P x, что эквивалентно P a и для всех x ∈ s, P x.

LaTeX

$$$\forall {P} {a} {s},\; \Big(\forall x, x \in \operatorname{insert} a s \Rightarrow P x\Big) \iff (P a \land \forall x \in s, P x)$$$

Lean4

theorem forall_mem_insert {P : α → Prop} {a : α} {s : Set α} : (∀ x ∈ insert a s, P x) ↔ P a ∧ ∀ x ∈ s, P x := by grind

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