imp — Mathlib

English

If p x implies q x for all x, then VectorAllP p v implies VectorAllP q v for any v.

Русский

Если p x → q x для всех x, то VectorAllP p v → VectorAllP q v для любого вектора v.

LaTeX

$$$\big(\forall x, p(x) \to q(x)\big) \to \big(\mathrm{VectorAllP}(p,v) \to \mathrm{VectorAllP}(q,v)\big).$$$

Lean4

theorem imp {p q : α → Prop} (h : ∀ x, p x → q x) {v : Vector3 α n} (al : VectorAllP p v) : VectorAllP q v :=
  (vectorAllP_iff_forall _ _).2 fun _ => h _ <| (vectorAllP_iff_forall _ _).1 al _

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