compl_mem_of_notMem

Mathlib.Order.PrimeIdeal

URI: https://scilib.ai/kg/mathlib#Order.Ideal.IsPrime.compl_mem_of_notMem

English

If hI is prime and x ∉ I, then xᶜ ∈ I.

Русский

Если hI простое, и x ∉ I, то xᶜ ∈ I.

LaTeX

$$$x\\notin I \\Rightarrow x^c \\in I$ under prime assumption$$

Lean4

theorem compl_mem_of_notMem (hI : IsPrime I) (hxnI : x ∉ I) : xᶜ ∈ I :=
  hI.mem_or_compl_mem.resolve_left hxnI

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

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

Разделы

Аффилиация

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