op_smul_inter_ne_empty_iff — Mathlib

English

In opposite-action context, the smul-intersection non-emptiness criterion reduces to a/b relations.

Русский

В контексте противоположного действия не пустота пересечения эквивалентна отношению a/b.

LaTeX

$$$x\cdot s \cap t \neq \emptyset \iff \exists a,b\ (a\in t \land b\in s) \land a^{-1} \cdot b = x.$$$

Lean4

@[to_additive]
theorem op_smul_inter_ne_empty_iff {s t : Set α} {x : αᵐᵒᵖ} :
    x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = MulOpposite.unop x :=
  by
  rw [← nonempty_iff_ne_empty]
  constructor
  · rintro ⟨a, h, ha⟩
    obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h
    exact ⟨b, x • b, ⟨hb, ha⟩, by simp⟩
  · rintro ⟨a, b, ⟨ha, hb⟩, H⟩
    have : MulOpposite.op (a⁻¹ * b) = x := congr_arg MulOpposite.op H
    exact ⟨b, mem_inter (mem_smul_set.mpr ⟨a, ha, by simp [← this]⟩) hb⟩

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