upper_two_blockTriangular — Mathlib

English

The matrix formed from blocks A,B;0,D is block triangular with respect to Sum.elim a b when a < b.

Русский

Матрица из блоков A,B;0,D блочно-треугольна по сумме блоков с разметкой Sum.elim a b при a < b.

LaTeX

$$$\BlockTriangular\bigl(fromBlocks\; A\; B\; 0\; D\bigr)\; (\mathrm{Sum}.elim(\lambda x. a)(\lambda x. b))$ при $a < b$$$

Lean4

theorem upper_two_blockTriangular [Zero R] [Preorder α] (A : Matrix m m R) (B : Matrix m n R) (D : Matrix n n R)
    {a b : α} (hab : a < b) : BlockTriangular (fromBlocks A B 0 D) (Sum.elim (fun _ => a) fun _ => b) := by
  rintro (c | c) (d | d) hcd <;>
    first
    | simp [hab.not_gt] at hcd ⊢

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