sub_iff_right — Mathlib

English

In an AddGroup, BlockTriangular (M - N) b is equivalent to BlockTriangular N b if M is BlockTriangular b.

Русский

В группе сложения, если M блочно-треугольна по b, то BlockTriangular (M - N) по b эквивалентно BlockTriangular N по b.

LaTeX

$$$\BlockTriangular\, M\, b \Rightarrow (\BlockTriangular\,(M-N)\, b \iff \BlockTriangular\, N\, b)$$$

Lean4

theorem sub_iff_right [AddGroup R] (hM : BlockTriangular M b) : BlockTriangular (M - N) b ↔ BlockTriangular N b :=
  ⟨(by simpa using ·.neg.add hM), hM.sub⟩

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