toNatSubmodule_toAddSubmonoid — Mathlib

English

A simplification lemma relating sSup of a set of submodules and sSup of their AddSubmonoid images.

Русский

Упрощённая лемма, связывающая sSup множества подмодулей и sSup изображений в AddSubmonoid.

LaTeX

$$Lemma (simp) sSup relation between Submodule and AddSubmonoid images$$

Lean4

@[simp]
theorem toNatSubmodule_toAddSubmonoid (S : AddSubmonoid M) : S.toNatSubmodule.toAddSubmonoid = S :=
  AddSubmonoid.toNatSubmodule.symm_apply_apply S

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