fromRows_isTotallyUnimodular_iff_rows

English

Equivalence: (fromRows A B) is TU iff A is TU, provided B has rowwise unit-like structure.

Русский

Эквивалентность: (fromRows A B) тотально унимодулярна тогда и только тогда, когда A такова, при условии, что B имеет строковую структуру единичного типа.

LaTeX

$$IsTotallyUnimodular((fromRows A B)) \\iff IsTotallyUnimodular(A)$$

Lean4

/-- If `A` is totally unimodular and each row of `B` is all zeros except for at most a single `1`,
then `fromRows A B` is totally unimodular. -/
theorem fromRows_isTotallyUnimodular_iff_rows [DecidableEq n] {A : Matrix m n R} {B : Matrix m' n R}
    (hB : Nonempty n → ∀ i : m', ∃ j : n, ∃ s : SignType, B i = Pi.single j s.cast) :
    (fromRows A B).IsTotallyUnimodular ↔ A.IsTotallyUnimodular :=
  ⟨.submatrix Sum.inl id, fun hA => hA.fromRows_unitlike hB⟩

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