toSubmodule_comap — Mathlib

English

The comap operation is associative: (s.comap g).comap f = s.comap (g ∘ f).

Русский

Операция взятия обратного образа замкнутого подпмодуля по двум отображениям ассоциативна: (s.comap g).comap f = s.comap (g ∘ f).

LaTeX

$$$ (s.comap g).comap f = s.comap (g \circ f).$$$

Lean4

@[simp]
theorem toSubmodule_comap (f : M →L[R] N) (s : ClosedSubmodule R N) : (s.comap f).toSubmodule = s.toSubmodule.comap f :=
  rfl

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