ciInf_set_eq — Mathlib

English

Let s be a nonempty subset of β and f: β → α. If a is the greatest lower bound of the image {f(i) : i ∈ s}, then the infimum of f over s equals a; i.e., ⨅ i ∈ s, f(i) = a.

Русский

Пусть s — непустое подмножество β и f: β → α. Если a является наибольшей нижней гранью множества изображений {f(i) : i ∈ s}, то infimum f над s равен a; то есть ⨅ i ∈ s, f(i) = a.

LaTeX

$$$\left(a = \inf\{ f(i) \mid i \in s\}\right) \land \left(s \neq \varnothing\right) \implies \inf_{i \in s} f(i) = a.$$$

Lean4

theorem ciInf_set_eq {s : Set β} {f : β → α} (H : IsGLB (f '' s) a) (Hne : s.Nonempty) : ⨅ i : s, f i = a :=
  IsGLB.csInf_eq (image_eq_range f s ▸ H) (image_eq_range f s ▸ Hne.image f)

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