offDiag_inter — Mathlib

English

The off-diagonal of the intersection equals the intersection of off-diagonals: (S ∩ T).offDiag = S.offDiag ∩ T.offDiag.

Русский

Вне диагонали пересечения равны пересечению вне диагоналей.

LaTeX

$$$(s \\cap t).\\mathrm{offDiag} = s.\\mathrm{offDiag} \\cap t.\\mathrm{offDiag}$$$

Lean4

theorem offDiag_inter : (s ∩ t).offDiag = s.offDiag ∩ t.offDiag :=
  coe_injective <| by
    push_cast
    exact Set.offDiag_inter _ _

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