English
A general version of smul_preimage_setₛₗ: if c acts surjectively on α and σ c acts injectively on β, then f⁻¹'(σ c • t) = c • f⁻¹'(t).
Русский
Обобщённая версия: если умножение на c по α сюръективно, а умножение на σ c по β инъективно, то f⁻¹'(σ c • t) = c • f⁻¹'(t).
LaTeX
$$f^{-1}(\sigma(c) \cdot t) = c \cdot f^{-1}(t)$$
Lean4
/-- General version of `preimage_smul_setₛₗ`.
This version assumes that the scalar multiplication by `c` is surjective
while the scalar multiplication by `σ c` is injective. -/
@[to_additive /-- General version of `preimage_vadd_setₛₗ`.
This version assumes that the vector addition of `c` is surjective
while the vector addition of `σ c` is injective. -/
]
theorem preimage_smul_setₛₗ' {c : M} (hc : Function.Surjective (fun (m : α) ↦ c • m))
(hc' : Function.Injective (fun (n : β) ↦ σ c • n)) : f ⁻¹' (σ c • t) = c • f ⁻¹' t :=
by
refine Subset.antisymm ?_ (smul_preimage_set_subsetₛₗ f c t)
rw [subset_def, hc.forall]
rintro x ⟨y, hy, hxy⟩
rw [map_smulₛₗ, hc'.eq_iff] at hxy
subst y
exact smul_mem_smul_set hy
