English
FromBlocks is injective on quadruples of blocks: fromBlocks A B C D = fromBlocks A' B' C' D' iff A = A' ∧ B = B' ∧ C = C' ∧ D = D'.
Русский
FromBlocks инъективна по каждой паре блоков: fromBlocks A B C D = fromBlocks A' B' C' D' тогда и только тогда A = A' ∧ B = B' ∧ C = C' ∧ D = D'.
LaTeX
$$fromBlocks_inj {A B C D} {A' B' C' D'} : fromBlocks A B C D = fromBlocks A' B' C' D' ↔ A = A' ∧ B = B' ∧ C = C' ∧ D = D'$$
Lean4
@[simp]
theorem fromBlocks_inj {A : Matrix n l α} {B : Matrix n m α} {C : Matrix o l α} {D : Matrix o m α} {A' : Matrix n l α}
{B' : Matrix n m α} {C' : Matrix o l α} {D' : Matrix o m α} :
fromBlocks A B C D = fromBlocks A' B' C' D' ↔ A = A' ∧ B = B' ∧ C = C' ∧ D = D' :=
ext_iff_blocks
