compl_F_eq_I

Mathlib.Order.PrimeIdeal

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

English

In a PrimePair, the complement of F is I: (IF.F : Set P)ᶜ = IF.I.

Русский

В паре PrimePair дополнение к F равно I: (IF.F)ᶜ = IF.I.

LaTeX

$$$ (IF.F : Set P)^{\\complement} = IF.I $$$

Lean4

theorem compl_F_eq_I : (IF.F : Set P)ᶜ = IF.I :=
  IF.isCompl_I_F.eq_compl.symm

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

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

Разделы

Аффилиация

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