sSup_N

Mathlib.RingTheory.Filtration

URI: https://scilib.ai/kg/mathlib#Ideal.Filtration.sSup_N

English

The sSup_N theorem states that the N-component of sSup equals the sup of the N-components: (sSup S).N = sSup (N '' S).

Русский

Компонента N от sSup равна наибольшему верхнему пределу компонент N: (sSup S).N = sSup (N '' S).

LaTeX

$$(sSup S).N = sSup (Ideal.Filtration.N '' S)$$

Lean4

@[simp]
theorem sSup_N (S : Set (I.Filtration M)) : (sSup S).N = sSup (Ideal.Filtration.N '' S) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru