inter_left — Mathlib

English

If F is stable, then the infimum with any F' again yields stability: (F' ⊓ F).Stable.

Русский

Если F стабильна, то пересечение с любой другой филтрацией F' снова даёт устойчивость: (F' ⊓ F).Stable.

LaTeX

$$$\\text{If } F\\text{ is Stable, then } (F' \\sqcap F).Stable.$$$

Lean4

theorem inter_left [IsNoetherianRing R] [Module.Finite R M] (hF : F.Stable) : (F' ⊓ F).Stable :=
  hF.of_le inf_le_right

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