supported_iInter — Mathlib

English

The supported submodule on an intersection is the infimum of the parts.

Русский

Подмодуль на пересечении равен инфиминуму соответствующих подмодулей.

LaTeX

$$$\mathrm{supported}(M,R,\bigcap_i s_i) = \bigwedge_i \mathrm{supported}(M,R,s_i)$$$

Lean4

theorem supported_iInter {ι : Type*} (s : ι → Set α) : supported M R (⋂ i, s i) = ⨅ i, supported M R (s i) :=
  Submodule.ext fun x => by simp [mem_supported, subset_iInter_iff]

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