forall_of_forall_cons — Mathlib

English

If p holds for every x in cons a s h, then in particular it holds for every x ∈ s.

Русский

Если p выполняется для каждого x в cons a s h, то в частности для каждого x ∈ s.

LaTeX

$$$(H) : \forall x, x \in\ cons\ a\ s\ h \to p\ x \Rightarrow \forall x, x \in s \to p\ x$$$

Lean4

/-- Useful in proofs by induction. -/
theorem forall_of_forall_cons {p : α → Prop} {h : a ∉ s} (H : ∀ x, x ∈ cons a s h → p x) (x) (h : x ∈ s) : p x :=
  H _ <| mem_cons.2 <| Or.inr h

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