orderBot — Mathlib

English

For any a, the bottom element of the upper-sets { x ∈ α | a ≤ x } is the point ⟨a, le_rfl⟩.

Русский

Для любого a нижняя граница над множеством { x ∈ α | a ≤ x } равна ⟨a, le_rfl⟩.

LaTeX

$$$\\min\\{ x \\in { x : α // a \\le x } \\} = \\langle a, \\mathrm{le\\_rfl} \\rangle$$$

Lean4

/-- This instance uses data fields from `Subtype.partialOrder` to help type-class inference.
The `Set.Ici` data fields are definitionally equal, but that requires unfolding semireducible
definitions, so type-class inference won't see this. -/
instance orderBot [Preorder α] {a : α} : OrderBot { x : α // a ≤ x } :=
  { Set.Ici.orderBot with }

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