ciSup_mem_image — Mathlib

English

For a nonempty Finset with a certain property, the ciSup (continuous supremum) image contains that image.

Русский

Для непустого Finset выполняется, что ciSup образа содержит этот образ.

LaTeX

$$$(h : ∃ x \in s, sSup ∅ ≤ f x) : ⨆ i ∈ s, f i ∈ s.image f$$$

Lean4

theorem ciSup_mem_image {s : Finset ι} (h : ∃ x ∈ s, sSup ∅ ≤ f x) : ⨆ i ∈ s, f i ∈ s.image f :=
  by
  rw [ciSup_eq_max'_image _ h]
  exact max'_mem (image f s) _

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