instOrderBot — Mathlib

English

There is a bottom ideal when P has a bottom element; the bottom is given by principal ⊥.

Русский

Существет нижний идеал, когда P имеет нижний элемент; нижний задаётся как principal(⊥).

LaTeX

$$OrderBot(P) ⇒ (∃ bottom_ideal, bottom_ideal = principal(⊥))$$

Lean4

/-- There is a bottom ideal when `P` has a bottom element. -/
instance : OrderBot (Ideal P) where
  bot := principal ⊥
  bot_le := by simp

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