mem_torsionBySet_iff — Mathlib

English

x ∈ torsionBySet R M s iff ∀ a ∈ s, a · x = 0.

Русский

x ∈ torsionBySet(R,M,s) эквивалентно ∀ a ∈ s, a · x = 0.

LaTeX

$$x ∈ torsionBySet(R,M,s) ↔ ∀ a ∈ s, a • x = 0$$

Lean4

@[simp]
theorem mem_torsionBySet_iff (x : M) : x ∈ torsionBySet R M s ↔ ∀ a : s, (a : R) • x = 0 :=
  by
  refine ⟨fun h ⟨a, ha⟩ => mem_sInf.mp h _ (Set.mem_image_of_mem _ ha), fun h => mem_sInf.mpr ?_⟩
  rintro _ ⟨a, ha, rfl⟩; exact h ⟨a, ha⟩

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