smul_inter_ne_empty_iff — Mathlib

English

Disjointness 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]
theorem smul_inter_ne_empty_iff {s t : Set α} {x : α} : x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x :=
  by
  rw [← nonempty_iff_ne_empty]
  constructor
  · rintro ⟨a, h, ha⟩
    obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h
    exact ⟨x • b, b, ⟨ha, hb⟩, by simp⟩
  · rintro ⟨a, b, ⟨ha, hb⟩, rfl⟩
    exact ⟨a, mem_inter (mem_smul_set.mpr ⟨b, hb, by simp⟩) ha⟩

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