orderIsoMapComap_symm_apply — Mathlib

English

For S : ι → Submodule R M, (⨆ i, (S i).map f).comap f = iSup S.

Русский

Для S: ι → Submodule R M выполняется: обратный образ суммы образов равен iSup(S).

LaTeX

$$$\forall {\iota : Sort*} (S : ι → Submodule R M), (⨆ i, (S i).map f).comap f = iSup S$$

Lean4

@[simp]
theorem orderIsoMapComap_symm_apply [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R₂ M₂) :
    (orderIsoMapComap f).symm p = comap f p :=
  rfl

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