support_single_disjoint — Mathlib

English

If b ≠ 0 and b' ≠ 0, then for all i, j ∈ α, the supports of single i b and single j b' are disjoint iff i ≠ j.

Русский

Пусть b ≠ 0 и b' ≠ 0. Для любых i, j ∈ α множества опор функций single(i,b) и single(j,b') пересекаются тогда и только тогда, когда i ≠ j.

LaTeX

$$$b \neq 0 \land b' \neq 0 \Rightarrow \operatorname{Disjoint}(\operatorname{supp}(\mathrm{single}(i,b)), \operatorname{supp}(\mathrm{single}(j,b'))) \iff i \neq j$$$

Lean4

theorem support_single_disjoint {b' : M} (hb : b ≠ 0) (hb' : b' ≠ 0) {i j : α} :
    Disjoint (single i b).support (single j b').support ↔ i ≠ j := by
  rw [support_single_ne_zero _ hb, support_single_ne_zero _ hb', disjoint_singleton]

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