sInf_image_Icc — Mathlib

English

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

Русский

Пусть f антинтонна на Icc[a,b]. Тогда inf{ 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': AntitoneOn f (Icc a b)) : sInf (f '' Icc a b) = f b$$$

Lean4

theorem sInf_image_Icc [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {a b : α} (hab : a ≤ b)
    (h' : AntitoneOn f (Icc a b)) : sInf (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_left.sInf_image_Icc (α := αᵒᵈ) hab

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