isTorsionBySet_iff_torsionBySet_eq_top

English

IsTorsionBySet s holds iff torsionBySet s = top.

Русский

IsTorsionBySet s эквивалентно torsionBySet s = верхушка.

LaTeX

$$$IsTorsionBySet\,R\,M\,s \;\iff\; torsionBySet\,R\,M\,s = \top$$$

Lean4

theorem isTorsionBySet_iff_torsionBySet_eq_top : IsTorsionBySet R M s ↔ torsionBySet R M s = ⊤ :=
  ⟨fun h => eq_top_iff.mpr fun _ _ => (mem_torsionBySet_iff _ _).mpr <| @h _, fun h x =>
    by
    rw [← mem_torsionBySet_iff, h]
    trivial⟩

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