ciInf_mem_image — Mathlib

English

Let s be a finite subset of ι and f: ι → α. Then the infimum of the values f(i) for i ∈ s lies in the image f''s, i.e. there exists i ∈ s with f(i) = inf{ f(j) : j ∈ s }. (This is the Set-level version of ciInf_mem_image.)

Русский

Пусть s—конечное подмножество индексов ι и f: ι → α. Тогда инфimum значений f(i) по i ∈ s лежит в образе f''s, то есть существует i ∈ s такое, что f(i) = inf{ f(j) : j ∈ s }. (Это версия для множеств.)

LaTeX

$$$\exists i \in s, f(i) = \inf_{j\in s} f(j).$$$

Lean4

theorem ciInf_mem_image {s : Set ι} (hs : s.Finite) (h : ∃ x ∈ s, f x ≤ sInf ∅) : ⨅ i ∈ s, f i ∈ f '' s :=
  by
  lift s to Finset ι using hs
  simp only [Finset.mem_coe] at h
  simpa using Finset.ciInf_mem_image f h

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