sSup_image_Icc — Mathlib

English

Let f be antitone on Icc[a,b]. Then the supremum of f''Icc[a,b] equals f(a).

Русский

Пусть f антинтонна на Icc[a,b]. Тогда sup{ f(x) : x ∈ Icc[a,b] } = f(a).

LaTeX

$$$[Preorder\ \alpha][ConditionallyCompleteLattice\ \beta]\ {f:\alpha\to\beta}\ {a,b:\alpha}\ (hab: a \le b) (h': AntitoneOn f (Icc a b)) : sSup (f '' Icc a b) = f a$$$

Lean4

theorem sSup_image_Icc [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {a b : α} (hab : a ≤ b)
    (h' : AntitoneOn f (Icc a b)) : sSup (f '' Icc a b) = f a :=
  h'.dual_right.sInf_image_Icc hab

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