blockTriangular_single — Mathlib

English

If b i ≤ b j, then the single entry matrix with indices i,j is block triangular with respect to b, for any c ∈ R.

Русский

Если b(i) ≤ b(j), то матрица-одиночка с единицами на i,j блочно-треугольна по b (для любого c).

LaTeX

$$$\BlockTriangular\bigl(\mathrm{single}\; i\; j\; c\bigr)\; b$, если $b(i) ≤ b(j)$$$

Lean4

theorem blockTriangular_single {i j : m} (hij : b i ≤ b j) (c : R) : BlockTriangular (single i j c) b :=
  by
  intro r s hrs
  apply single_apply_of_ne
  rintro ⟨rfl, rfl⟩
  exact (hij.trans_lt hrs).false

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