supported_inter — Mathlib

English

The intersection of supports corresponds to the infimum of the corresponding submodules.

Русский

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

LaTeX

$$$\mathrm{supported}(M,R,s\cap t) = \mathrm{supported}(M,R,s) \cap \mathrm{supported}(M,R,t)$$$

Lean4

theorem supported_inter (s t : Set α) : supported M R (s ∩ t) = supported M R s ⊓ supported M R t := by
  rw [Set.inter_eq_iInter, supported_iInter, iInf_bool_eq]; rfl

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