ite_apply — Mathlib

English

Operator ite acts componentwise: ite P A B i j = ite P (A i j) (B i j).

Русский

Оператор ite действует по элементам: ite P A B i j = ite P (A i j) (B i j).

LaTeX

$$$ \forall P\; [Decidable P],\ A,B : Matrix m n \alpha,\ i : m,\ j : n,\ ite P A B i j = ite P (A i j) (B i j)$$$

Lean4

protected theorem ite_apply (P : Prop) [Decidable P] (A : Matrix m n α) (B : Matrix m n α) (i : m) (j : n) :
    (if P then A else B) i j = if P then A i j else B i j :=
  Matrix.dite_apply _ _ _ _ _

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