blockTriangular_single' — Mathlib

English

If hij: b j ≤ b i, then BlockTriangular (single i j c) with respect to the dual labeling toDual ∘ b.

Русский

Если b j ≤ b i, то BlockTriangular (single i j c) относительно двойной разметки toDual ∘ b.

LaTeX

$$$\BlockTriangular\bigl(\mathrm{single}\; i\; j\; c\bigr)\; (toDual \circ b)$, при $b j ≤ b i$$$

Lean4

theorem blockTriangular_single' {i j : m} (hij : b j ≤ b i) (c : R) : BlockTriangular (single i j c) (toDual ∘ b) :=
  blockTriangular_single (by exact toDual_le_toDual.mpr hij) _

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