lt_sup — Mathlib

English

For any x ∈ s, r x (wf.sup s h) holds; i.e., each element of s is below the supremum.

Русский

Для любого x ∈ s выполняется r x (sup s), то есть каждый элемент s ниже наибольшего предела.

LaTeX

$$$\\forall x\\in s,\\; r\\ x\\ (\\text{wf.sup }s\\ h)$$$

Lean4

protected theorem lt_sup {r : α → α → Prop} (wf : WellFounded r) {s : Set α} (h : Bounded r s) {x} (hx : x ∈ s) :
    r x (wf.sup s h) :=
  min_mem wf {x | ∀ a ∈ s, r a x} h x hx

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