le_of_le — Mathlib

English

Let (α, ≤) be a poset, and P a predicate on α. If x is a P-minimal element and y also satisfies P, and y ≤ x, then x ≤ y.

Русский

Пусть (α, ≤) — частично упорядченное множество, и P — предикат на α. Если x является минимальным относительно P и y удовлетворяет P, и y ≤ x, тогда выполняется x ≤ y.

LaTeX

$$$\\\\forall α \, (\\\\le) \, (P: α \\\\to \\\\mathrm{Prop}) \, (x,y : α), \\\\operatorname{Min}_P(x) \\\\land \\\\operatorname{P}(y) \\\\land y \\\\le x \\\\Rightarrow x \\\\le y.$$$

Lean4

theorem le_of_le (h : Minimal P x) (hy : P y) (hle : y ≤ x) : x ≤ y :=
  h.2 hy hle

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