vectorAllP_cons — Mathlib

English

VectorAllP p (x :: v) holds iff p x holds and VectorAllP p v holds; i.e., the conjunction splits at the head.

Русский

VectorAllP p (x :: v) эквивалентно p x ∧ VectorAllP p v; конъюнкция разлагается по голове.

LaTeX

$$$\mathrm{VectorAllP}(p,\mathrm{cons}(x,v)) \iff p(x) \land \mathrm{VectorAllP}(p,v).$$$

Lean4

@[simp]
theorem vectorAllP_cons (p : α → Prop) (x : α) (v : Vector3 α n) : VectorAllP p (x :: v) ↔ p x ∧ VectorAllP p v :=
  Vector3.recOn v (iff_of_eq (and_true _)).symm fun _ _ _ => Iff.rfl

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