instOrderBot — Mathlib

English

Part α is equipped with a bottom element none, and this bottom is ≤ every element: none ≤ x for all x ∈ Part α.

Русский

Часть α снабжена нижним элементом none, и этот нижний элемент меньше или равен любому элементу: none ≤ x для всех x ∈ Part α.

LaTeX

$$$ \text{bot} = none, \ \forall x : \mathrm{Part}(\alpha), \ \\bot \\le x $$$

Lean4

instance : OrderBot (Part α) where
  bot := none
  bot_le := by rintro x _ ⟨⟨_⟩, _⟩

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