mem_doublyStochastic — Mathlib

English

A matrix M belongs to the set of doubly stochastic matrices if and only if it has nonnegative entries and both row and column sums equal 1.

Русский

Матрица M принадлежит множеству двойственно стохастических, если и только если все ее элементы неотрицательны, а суммы по строкам и по столбцам равны 1.

LaTeX

$$$M\in\,doublyStochastic(R,n) \iff (\forall i,j, M_{ij} \ge 0) \land (M\mathbf{1}=\mathbf{1}) \land (\mathbf{1}^T M=\mathbf{1}^T).$$$

Lean4

theorem mem_doublyStochastic : M ∈ doublyStochastic R n ↔ (∀ i j, 0 ≤ M i j) ∧ M *ᵥ 1 = 1 ∧ 1 ᵥ* M = 1 :=
  Iff.rfl

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