smul_inter_ne_empty_iff' — Mathlib

English

Similarly, disjointness is preserved for additive actions; i.e., for AddGroup actions, smul preserves disjointness.

Русский

Аналогично для аддитивных действий: умножение сохраняет несовпадение.

LaTeX

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

Lean4

@[to_additive]
theorem smul_inter_ne_empty_iff' {s t : Set α} {x : α} : x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a / b = x := by
  simp_rw [smul_inter_ne_empty_iff, div_eq_mul_inv]

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