smul_preimage_set_subset

Mathlib.GroupTheory.GroupAction.Pointwise

URI: https://scilib.ai/kg/mathlib#smul_preimage_set_subset

English

If f maps 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 • f⁻¹(t) ⊆ f⁻¹(c • t).

LaTeX

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

Lean4

@[to_additive]
theorem smul_preimage_set_subset (f : F) (c : M) (t : Set β) : c • f ⁻¹' t ⊆ f ⁻¹' (c • t) :=
  smul_preimage_set_subsetₛₗ f c t

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru