dite_apply — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

protected theorem dite_apply (P : Prop) [Decidable P] (A : P → Matrix m n α) (B : ¬P → Matrix m n α) (i : m) (j : n) :
    dite P A B i j = dite P (A · i j) (B · i j) := by rw [dite_apply, dite_apply]

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