offDiag_insert — Mathlib

English

If a is not in s, then the off-diagonal of insert a s equals s.offDiag together with the cross products with a at either side.

Русский

Если a не принадлежит s, то вне диагонали вставки a в s равна объединению s.offDiag с {a}×s и s×{a}.

LaTeX

$$$ (insert\ a\ s).offDiag = s.offDiag \cup { a } \times s \cup s \times { a } $$$

Lean4

theorem offDiag_insert (ha : a ∉ s) : (insert a s).offDiag = s.offDiag ∪ { a } ×ˢ s ∪ s ×ˢ { a } := by grind

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