le_of_ge — Mathlib

English

Let (α, ≤) be a poset, and P a predicate on α. If x is a maximal element with respect to P and y ∈ P and x ≤ y, then y ≤ x.

Русский

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

LaTeX

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

Lean4

theorem le_of_ge (h : Maximal P x) (hy : P y) (hge : x ≤ y) : y ≤ x :=
  h.2 hy hge

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