instCompleteLattice

Mathlib.RingTheory.Filtration

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

← MathLib Explorer

English

The collection of I-filtrations of M forms a complete lattice.

Русский

Множество I-фильтраций M образует полную решётку.

LaTeX

$$I.Filtration M is a complete lattice$$

Lean4

instance : CompleteLattice (I.Filtration M) :=
  Function.Injective.completeLattice Ideal.Filtration.N (fun _ _ => Ideal.Filtration.ext) sup_N inf_N
    (fun _ => sSup_image) (fun _ => sInf_image) top_N bot_N

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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