forall_of_forall_insert — Mathlib

English

If a property p holds for all elements of insert a s, then it also holds for all x in s.

Русский

Если свойство p выполняется для всех элементов insert a s, то оно выполняется и для всех x из s.

LaTeX

$$$\\forall {α} {p : α \\to Prop} {a} {s : Finset α},\\ (\\forall x, x \\in \\operatorname{insert} a s \\rightarrow p x) \\rightarrow \\forall x, x \\in s \\rightarrow p x.$$$

Lean4

/-- Useful in proofs by induction. -/
theorem forall_of_forall_insert {p : α → Prop} {a : α} {s : Finset α} (H : ∀ x, x ∈ insert a s → p x) (x) (h : x ∈ s) :
    p x :=
  H _ <| mem_insert_of_mem h

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