not_infIrred_top

Mathlib.Order.Irreducible

URI: https://scilib.ai/kg/mathlib#not_infIrred_top

English

For SupPrime a, a ≤ s.sup f iff there exists i ∈ s with a ≤ f i.

Русский

Для SupPrime a верно, что a ≤ s.sup f тогда и только тогда, когда существует i ∈ s такое, что a ≤ f i.

LaTeX

$$SupPrime\ a \rightarrow (a \le s.sup f) \leftrightarrow (\exists i ∈ s, a \le f i)$$

Lean4

theorem not_infIrred_top : ¬InfIrred (⊤ : α) :=
  isMax_top.not_infIrred

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

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

Разделы

Аффилиация

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