English
If s and t are disjoint, then the off-diagonal of s ∪ t equals the union of off-diagonals plus the cross products across s and t.
Русский
Если s и t непересекаются, то offDiag(s ∪ t) равен объединению offDiag(s), offDiag(t) и перекрёстных произведений между s и t.
LaTeX
$$$ (s \cup t).offDiag = s.offDiag \cup t.offDiag \cup s \times t \cup t \times s \quad \text{if } Disjoint\ s s, t $$$
Lean4
theorem offDiag_union (h : Disjoint s t) : (s ∪ t).offDiag = s.offDiag ∪ t.offDiag ∪ s ×ˢ t ∪ t ×ˢ s :=
by
ext x
simp only [mem_offDiag, mem_union, ne_eq, mem_prod]
constructor
· rintro ⟨h0 | h0, h1 | h1, h2⟩ <;> simp [h0, h1, h2]
· rintro (((⟨h0, h1, h2⟩ | ⟨h0, h1, h2⟩) | ⟨h0, h1⟩) | ⟨h0, h1⟩) <;> simp [*]
· rintro h3
rw [h3] at h0
exact Set.disjoint_left.mp h h0 h1
· rintro h3
rw [h3] at h0
exact (Set.disjoint_right.mp h h0 h1).elim
