inf_submodule — Mathlib

English

The construction F.submodule can be viewed as an InfHom from the lattice of filtrations to the lattice of submodules; in particular, there is a map that preserves infima: the submodule of the infimum is the infimum of submodules.

Русский

Установление подмодуля можно рассматривать как отображение, сохраняющее пересечения: подмодуль пересечения фильтраций равен пересечению соответствующих подмодулей.

LaTeX

$$The map F ↦ F.submodule is an InfHom, i.e., map_inf' = inf_submodule.$$

Lean4

theorem inf_submodule : (F ⊓ F').submodule = F.submodule ⊓ F'.submodule :=
  by
  ext
  exact forall_and

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