isProper

Mathlib.Order.Ideal

URI: https://scilib.ai/kg/mathlib#IsCoatom.isProper

English

If I is a coatom, then I is proper.

Русский

Если I является коатомом, то он правильный.

LaTeX

$$IsCoatom(I) \Rightarrow IsProper(I)$$

Lean4

theorem _root_.IsCoatom.isProper (hI : IsCoatom I) : IsProper I :=
  isProper_of_ne_top hI.1

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

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

Разделы

Аффилиация

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