mem_inv_smul_set_iff — Mathlib

English

In a group action setting, membership is preserved under inverse image via the action map: x ∈ a⁻¹ • A iff a • x ∈ A.

Русский

При действии группы принадлежность сохраняется через образ обратного действия: x ∈ a⁻¹ • A ⇔ a • x ∈ A.

LaTeX

$$$\forall a\in α,\forall A\subseteq β:\ x\in a^{-1}\cdot A \Leftrightarrow a\cdot x\in A.$$$

Lean4

@[to_additive]
theorem mem_inv_smul_set_iff : x ∈ a⁻¹ • A ↔ a • x ∈ A := by
  simp only [← image_smul, mem_image, inv_smul_eq_iff, exists_eq_right]

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