supIrred

Mathlib.Order.Irreducible

URI: https://scilib.ai/kg/mathlib#SupPrime.supIrred

English

Every sup-Prime element is also sup-Irred.

Русский

Каждый элемент, являющийся SupPrime, также является SupIrred.

LaTeX

$$SupPrime\ a \rightarrow SupIrred\ a$$

Lean4

protected theorem supIrred : SupPrime a → SupIrred a :=
  And.imp_right fun h b c ha => by simpa [← ha] using h ha.ge

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

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

Разделы

Аффилиация

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