toBlock_one_disjoint — Mathlib

English

If two predicates p and q on the index set are disjoint, then the corresponding block of the block diagonal with 1 on the diagonal is zero.

Русский

Если две предикаты p и q на множестве индексов несовместны, соответствующий блок блочной диагонали с единицами на диагонали равен нулю.

LaTeX

$$$\operatorname{toBlock}_{\text{diag}}(1)\; p\; q = 0 \quad \text{whenever } \text{Disjoint}(p,q).$$$

Lean4

theorem toBlock_one_disjoint {p q : m → Prop} (hpq : Disjoint p q) : Matrix.toBlock (1 : Matrix m m α) p q = 0 :=
  toBlock_diagonal_disjoint _ hpq

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