top_of_top_mem

Mathlib.Order.Ideal

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

English

The principal of the bottom element equals the bottom ideal.

Русский

Прообраз главного нижнего элемента равен нижнему идеалу.

LaTeX

$$principal(\bot) = \bot$$

Lean4

theorem top_of_top_mem (h : ⊤ ∈ I) : I = ⊤ := by
  ext
  exact iff_of_true (I.lower le_top h) trivial

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

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

Разделы

Аффилиация

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