smul_preimage_set_subsetₛₗ — Mathlib

English

If f maps a set s into t, then the smul of the preimage by c is contained in the preimage of the smul: c • f⁻¹(t) ⊆ f⁻¹(σ c • t).

Русский

Если f отображает s в t, то умножение предобраза на c подчиняется: c • f⁻¹(t) ⊆ f⁻¹(σ c • t).

LaTeX

$$$c \cdot f^{-1}(t) \subseteq f^{-1}(\sigma(c) \cdot t)$$$

Lean4

/-- Translation of preimage is contained in preimage of translation -/
@[to_additive]
theorem smul_preimage_set_subsetₛₗ (f : F) (c : M) (t : Set β) : c • f ⁻¹' t ⊆ f ⁻¹' (σ c • t) :=
  ((mapsTo_preimage f t).smul_setₛₗ c).subset_preimage

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