offDiag_union — Mathlib

English

The off-diagonal of the union equals the union of off-diagonals plus cross terms: (S ∪ T).offDiag = S.offDiag ∪ T.offDiag ∪ S × T ∪ T × S.

Русский

Вне диагонали объединения равняется объединению вне диагоналей плюс поперечные пары: (S ∪ T).offDiag = S.offDiag ∪ T.offDiag ∪ S × T ∪ T × S.

LaTeX

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

Lean4

theorem offDiag_union (h : Disjoint s t) : (s ∪ t).offDiag = s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s :=
  coe_injective <| by
    push_cast
    exact Set.offDiag_union (disjoint_coe.2 h)

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