mulSupport_mulSingle_disjoint — Mathlib

English

For ha ≠ 1 and hb ≠ 1, the mulSupport of mulSingle i a and mulSingle j b are disjoint iff i ≠ j.

Русский

Если ha ≠ 1 и hb ≠ 1, то опоры mulSingle i a и mulSingle j b сопоставимы по дизъюнктности: они непересекаются тогда, когда i ≠ j.

LaTeX

$$$ \operatorname{Disjoint}(\operatorname{mulSupport}(\mathrm{Pi}.\mathrm{mulSingle} i a), \operatorname{mulSupport}(\mathrm{Pi}.\mathrm{mulSingle} j b)) \iff i \neq j $$$

Lean4

@[to_additive]
theorem mulSupport_mulSingle_disjoint (ha : a ≠ 1) (hb : b ≠ 1) :
    Disjoint (mulSupport (mulSingle i a)) (mulSupport (mulSingle j b)) ↔ i ≠ j := by
  rw [mulSupport_mulSingle_of_ne ha, mulSupport_mulSingle_of_ne hb, disjoint_singleton]

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