csSup_eq_of_subset_of_forall_exists_le

English

Let f be monotone on t, s ⊆ t with BddAbove for f''t. Then the supremum of f''s equals the supremum of f''t.

Русский

Пусть f монотонна на t, s ⊆ t и f''t ограничено сверху. Тогда sup { f(x) : x ∈ s } = sup { f(x) : x ∈ t }.

LaTeX

$$$[Preorder\ `\alpha][ConditionallyCompleteLattice\ \beta] \{f:\alpha\to\beta\}\; ht:\; BddAbove (f '' t) \rightarrow hf:\; MonotoneOn f t \rightarrow hst:\; s \subseteq t \rightarrow (\forall y \in t, \exists x \in s, y \le x) \rightarrow sSup (f '' s) = sSup (f '' t)$$$

Lean4

theorem csSup_eq_of_subset_of_forall_exists_le [Preorder α] [ConditionallyCompleteLattice β] {f : α → β} {s t : Set α}
    (ht : BddAbove (f '' t)) (hf : MonotoneOn f t) (hst : s ⊆ t) (h : ∀ y ∈ t, ∃ x ∈ s, y ≤ x) :
    sSup (f '' s) = sSup (f '' t) :=
  MonotoneOn.csInf_eq_of_subset_of_forall_exists_le (α := αᵒᵈ) (β := βᵒᵈ) ht hf.dual hst h

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