sSup_image_Icc — Mathlib

English

If f is monotone on the closed interval Icc[a,b], the supremum of the image f''Icc[a,b] is f(b).

Русский

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

LaTeX

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

Lean4

theorem sSup_image_Icc [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {a b : α} (hab : a ≤ b)
    (h' : MonotoneOn f (Icc a b)) : sSup (f '' Icc a b) = f b :=
  by
  have : Icc a b = Icc (α := αᵒᵈ) (toDual b) (toDual a) := by rw [Icc_toDual]; rfl
  rw [this] at h' ⊢
  exact h'.dual_right.dual_left.sInf_image_Icc (β := βᵒᵈ) (α := αᵒᵈ) hab

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