sup — Mathlib

English

The supremum of a bounded well-founded order is defined as the minimum of the set {x | ∀ a ∈ s, r a x}.

Русский

Супремум ограниченного хорошо основанного порядка определяется как минимум множества {x | для всех a ∈ s выполняется r a x}.

LaTeX

$$$\\text{sup}(wf)(s)(h) = \\min\\{ x : α \\mid \\forall a\\in s,\\ r\\ a\\ x\\}$$$

Lean4

/-- The supremum of a bounded, well-founded order -/
protected noncomputable def sup {r : α → α → Prop} (wf : WellFounded r) (s : Set α) (h : Bounded r s) : α :=
  wf.min {x | ∀ a ∈ s, r a x} h

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