apply — Mathlib

English

If A is totally unimodular and each row of B is zero except possibly for a single nonzero entry of ±1, then the matrix obtained by stacking A on top of B, i.e., fromRows A B, is totally unimodular.

Русский

Если A тотально унимодулярна, а каждая строка B состоит из нулей, за редким исключением одной единицы или одной −1, то матрица fromRows A B тоже тотально унимодулярна.

LaTeX

$$(fromRows A B).IsTotallyUnimodular$$

Lean4

theorem apply {A : Matrix m n R} (hA : A.IsTotallyUnimodular) (i : m) (j : n) : A i j ∈ Set.range SignType.cast :=
  by
  rw [isTotallyUnimodular_iff] at hA
  simpa using hA 1 (fun _ => i) (fun _ => j)

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