inter_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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