ext_iff — Mathlib

English

For DMatrix m n α, two elements are equal iff all corresponding entries agree.

Русский

Для DMatrix m n α два элемента равны тогда и только тогда, когда все соответствующие элементы согласованы.

LaTeX

$$$\\forall i, j,\\; M i j = N i j \\quad \\Leftrightarrow \\quad M = N$$$

Lean4

theorem ext_iff : (∀ i j, M i j = N i j) ↔ M = N :=
  ⟨fun h => funext fun i => funext <| h i, fun h => by simp [h]⟩

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