ciSup_set_eq — Mathlib

English

The coerced infimum equals the infimum taken in WithBot α.

Русский

Приведение к WithBot сохраняет инфимум: ↑(⨅ i, f i) = ⨅ i, f i в WithBot α.

LaTeX

$$$\uparrow\left(\inf_i f(i)\right) = \inf_i f(i)\quad\text{in } WithBot(\alpha)$$$

Lean4

theorem ciSup_set_eq {s : Set β} {f : β → α} (H : IsLUB (f '' s) a) (Hne : s.Nonempty) : ⨆ i : s, f i = a :=
  IsLUB.csSup_eq (image_eq_range f s ▸ H) (image_eq_range f s ▸ Hne.image f)

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