isTorsionBySet_of_subset

Mathlib.Algebra.Module.Torsion

URI: https://scilib.ai/kg/mathlib#Module.isTorsionBySet_of_subset

English

If s ⊆ t and t is torsion by set, then s is torsion by set.

Русский

Если s ⊆ t и t имеет торион по множеству, то и s имеет торион по множеству.

LaTeX

$$$\forall s,t\, (s \subseteq t)\; (IsTorsionBySet\,R\,M\, t) \Rightarrow IsTorsionBySet\,R\,M\, s$$$

Lean4

theorem isTorsionBySet_of_subset {s t : Set R} (h : s ⊆ t) (ht : IsTorsionBySet R M t) : IsTorsionBySet R M s :=
  fun m r ↦ @ht m ⟨r, h r.2⟩

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

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

Разделы

Аффилиация

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