isTorsionBySet_iff_subset_annihilator

English

For a set s ⊆ R, IsTorsionBySet R M s holds if and only if s ⊆ annihilator R M.

Русский

Для множества s ⊆ R выполняется IsTorsionBySet R M s тогда и только тогда, когда s ⊆ annihilator R M.

LaTeX

$${s : Set R} : IsTorsionBySet R M s ↔ s ⊆ annihilator R M$$

Lean4

theorem isTorsionBySet_iff_subset_annihilator {s : Set R} : IsTorsionBySet R M s ↔ s ⊆ annihilator R M :=
  by
  simp_rw [IsTorsionBySet, Set.subset_def, SetLike.mem_coe, mem_annihilator]
  rw [forall_comm, SetCoe.forall]

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