toBlock_diagonal_disjoint — Mathlib

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]

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