zero_le_one_elem — Mathlib

English

In a matrix with 0s and 1s on diagonal and off-diagonal, every entry of the identity matrix is nonnegative; i.e., 0 ≤ (1)_{ij} for all i,j.

Русский

Для единичной матрицы каждый элемент неотрицателен: 0 ≤ (1)_{ij} для всех i,j.

LaTeX

$$$0 \\le (1)_{ij}$ for all i,j.$$

Lean4

theorem zero_le_one_elem [Preorder α] [ZeroLEOneClass α] (i j : n) : 0 ≤ (1 : Matrix n n α) i j :=
  by
  by_cases hi : i = j
  · subst hi
    simp
  · simp [hi]

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