forall_of_forall_insert — Mathlib

English

If P holds for every x in insert a s, then P holds for every x in s.

Русский

Если P выполняется для каждого x ∈ insert a s, то P выполняется для каждого x ∈ s.

LaTeX

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

Lean4

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

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