English
Let S be a subset of α with 0 ∈ S. For any function d : n → α, the diagonal matrix with entries d(i) on the diagonal lies in S-matrix if and only if every diagonal entry d(i) belongs to S.
Русский
Пусть S ⊆ α и 0 ∈ S. Для любой функции d : n → α диагональная матрица с диагональными элементами d(i) принадлежит S-массива тогда и только тогда, когда каждый элемент диагонали d(i) принадлежит S.
LaTeX
$$$0 \in S \Rightarrow \bigl( \mathrm{diagonal}(d) \in S^{n \times n} \iff \forall i\, d(i) \in S \bigr)$$$
Lean4
theorem diagonal_mem_matrix_iff [Zero α] {S : Set α} (hS : 0 ∈ S) {d : n → α} :
Matrix.diagonal d ∈ S.matrix ↔ ∀ i, d i ∈ S :=
by
simp only [Set.mem_matrix, diagonal, of_apply]
conv_lhs => intro _ _; rw [ite_mem]
simp [hS]
