I_isProper

Mathlib.Order.PrimeIdeal

URI: https://scilib.ai/kg/mathlib#Order.Ideal.PrimePair.I_isProper

English

If (I,F) forms a PrimePair, then I is a proper ideal.

Русский

Если (I,F) образуют PrimePair, то I является proper идеал.

LaTeX

$$$I \\text{ is proper}$$$

Lean4

theorem I_isProper : IsProper IF.I := by
  obtain ⟨w, h⟩ := IF.F.nonempty
  apply isProper_of_notMem (_ : w ∉ IF.I)
  rwa [← IF.compl_I_eq_F] at h

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

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

Разделы

Аффилиация

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