preimage_smul₀ — Mathlib

English

Let a ≠ 0. For any set t ⊆ β, the preimage of t under the map x ↦ a • x equals a⁻¹ • t.

Русский

Пусть a ≠ 0. Для любого множества t ⊆ β предобраз отображения x ↦ a • x равно a⁻¹ • t.

LaTeX

$$$ (ha : a \neq 0) (t : Set β), \{ x : β | a \cdot x \in t \} = a^{-1} \cdot t $$$

Lean4

theorem preimage_smul₀ (ha : a ≠ 0) (t : Set β) : (fun x ↦ a • x) ⁻¹' t = a⁻¹ • t :=
  preimage_smul (Units.mk0 a ha) t

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