le_one_of_mem_doublyStochastic — Mathlib

English

Let M be a doubly stochastic matrix over R. Then every entry M_{ij} satisfies M_{ij} ≤ 1.

Русский

Пусть M — двоично стохастическая матрица надR. Тогда каждый элемент M_{ij} удовлетворяет M_{ij} ≤ 1.

LaTeX

$$$M \in \mathrm{doublyStochastic}(R,n) \Rightarrow \forall i,j\, M_{ij} \le 1$$$

Lean4

/-- Every entry of a doubly stochastic matrix is less than or equal to 1. -/
theorem le_one_of_mem_doublyStochastic (hM : M ∈ doublyStochastic R n) {i j : n} : M i j ≤ 1 :=
  by
  rw [← sum_row_of_mem_doublyStochastic hM i]
  exact single_le_sum (fun k _ => hM.1 _ k) (mem_univ j)

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