instOrderBotEq — Mathlib

English

For every a in a linearly ordered type α, the subset {x in α : x = a} carries a trivial order whose bottom element is a itself.

Русский

Для каждого a из линейно упорядоченного множества α подмножество {x ∈ α : x = a} наследует тривиальный порядок, у которого нижний элемент равен a.

LaTeX

$$$\text{Let } a \in \alpha. \; X = \{ x \in \alpha : x = a \}. \; \text{Then } X \text{ with the inherited order has } \bot = a. $$$

Lean4

/-- A local instance that enables using "the actual value" as a priority estimator,
for simple use cases. -/
local instance instOrderBotEq {a : α} : OrderBot { x : α // x = a }
    where
  bot := ⟨a, rfl⟩
  bot_le := by simp

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