forall_insert_of_forall — Mathlib

English

If for all x, x ∈ insert a s implies P x, and P a holds, then for all x ∈ s, P x holds.

Русский

Если для всех x, x ∈ insert a s → P x и P a, то для всех x ∈ s выполняется P x.

LaTeX

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

Lean4

theorem forall_insert_of_forall {P : α → Prop} {a : α} {s : Set α} (H : ∀ x, x ∈ s → P x) (ha : P a) (x)
    (h : x ∈ insert a s) : P x := by grind

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