image_subset_Iic_sup — Mathlib

English

For any f: ι → α and finite s ⊆ ι, the image s.image f is contained in Iic (s.sup f).

Русский

Для любого отображения f: ι → α и конечного множества s ⊆ ι образ s.image f лежит в Iic (s.sup f).

LaTeX

$$$ s.{\text{image}} f \subseteq Iic (s.\text{sup} f) $$$

Lean4

theorem image_subset_Iic_sup [OrderBot α] [DecidableEq α] (f : ι → α) (s : Finset ι) : s.image f ⊆ Iic (s.sup f) :=
  by
  refine fun i hi ↦ mem_Iic.2 ?_
  obtain ⟨j, hj, rfl⟩ := mem_image.1 hi
  exact le_sup hj

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