disjoint_smul_set — Mathlib

English

Disjointness is preserved under smul: Disjoint (a • s) (a • t) ⇔ Disjoint s t.

Русский

Несовпадение сохраняется под действием: Disjoint (a • s) (a • t) ⇔ Disjoint s t.

LaTeX

$$$\operatorname{Disjoint}(a\cdot s, a\cdot t) \iff \operatorname{Disjoint}(s,t).$$$

Lean4

@[to_additive (attr := simp)]
theorem disjoint_smul_set : Disjoint (a • s) (a • t) ↔ Disjoint s t :=
  disjoint_image_iff <| MulAction.injective _

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