English
If d: m → α and p, q are disjoint predicates, then the block of the diagonal matrix between p and q is zero: toBlock (diagonal d) p q = 0.
Русский
Если d: m → α и предикаты p и q несовместны, то блок диагональной матрицы между p и q равен нулю: toBlock (diagonal d) p q = 0.
LaTeX
$$$\\text{toBlock}(\\text{diagonal } d)\\; p\\; q = 0 \\quad\\text{if } \\mathrm{Disjoint}(p,q)$$$
Lean4
theorem toBlock_diagonal_disjoint (d : m → α) {p q : m → Prop} (hpq : Disjoint p q) :
Matrix.toBlock (diagonal d) p q = 0 := by
ext ⟨i, hi⟩ ⟨j, hj⟩
have : i ≠ j := fun heq => hpq.le_bot i ⟨hi, heq.symm ▸ hj⟩
simp [diagonal_apply_ne d this]