rel_prod — Mathlib

English

Let R be a relation on M,N with R 1 1 and hf a relator lifting for multiplication; then (Forall₂ R) List.prod List.prod holds: the componentwise relation is preserved by products.

Русский

Пусть R — отношение на M,N с R(1,1) и hf — отношение, сохраняющее умножение; тогда (Forall₂ R) List.prod List.prod сохраняет отношение через произведение.

LaTeX

$$$$\\text{rel_prod: } R 1 1 \\to (R \\Rightarrow R \\Rightarrow R) \\to (Forall₂ R) List.prod List.prod.$$$$

Lean4

@[to_additive]
theorem rel_prod {R : M → N → Prop} (h : R 1 1) (hf : (R ⇒ R ⇒ R) (· * ·) (· * ·)) : (Forall₂ R ⇒ R) prod prod :=
  rel_foldr hf h

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