preimage_smul — Mathlib

English

Let a ∈ α and t ⊆ β. The preimage of t under the map x ↦ a • x equals a⁻¹ • t.

Русский

Пусть a ∈ α и t ⊆ β. Тогда множество предобраза t по отображению x ↦ a • x равно a⁻¹ • t.

LaTeX

$$$\forall a\in α,\, t\subseteq β:\ (\{x\in β : a\cdot x\in t\}) = a^{-1}\cdot t.$$$

Lean4

@[to_additive]
theorem preimage_smul (a : α) (t : Set β) : (fun x ↦ a • x) ⁻¹' t = a⁻¹ • t :=
  ((MulAction.toPerm a).symm.image_eq_preimage _).symm

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