single_mem_matrix — Mathlib

English

Let S be a set of scalars with 0 ∈ S. The matrix with a single nonzero a at (i, j) lies in S-matrix iff a ∈ S.

Русский

Пусть S — множество скаляров с 0 ∈ S. Матрица, в которой единственный ненулевой элемент равен a в позиции (i, j), принадлежит S-матрицам тогда, когда a ∈ S.

LaTeX

$$$ (\mathrm{single}_{i j} a) \in S_{matrix} \iff a \in S $$$

Lean4

theorem single_mem_matrix {S : Set α} (hS : 0 ∈ S) {i : m} {j : n} {a : α} : Matrix.single i j a ∈ S.matrix ↔ a ∈ S :=
  by
  simp only [Set.mem_matrix, single, of_apply]
  conv_lhs => intro _ _; rw [ite_mem]
  simp [hS]

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