ciInf_subtype'' — Mathlib

English

Let Nonempty ι and s ⊆ ι with s.Nonempty. For f : ι → α and BddBelow (range f), the infimum over i ∈ s of f(i) equals the infimum over i : s of f(i).

Русский

Пусть непусто ι и s ⊆ ι, s непусто. Для f: ι → α с нижней ограниченностью, инфиму́м по i∈s f(i) равен инфиму́му по i∈s реализованному как элемент подмножества s.

LaTeX

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

Lean4

theorem ciInf_subtype'' {ι} [Nonempty ι] {s : Set ι} (hs : s.Nonempty) {f : ι → α}
    (hf : BddBelow (Set.range fun i : s ↦ f i)) (hf' : ⨅ i : s, f i ≤ sInf ∅) :
    ⨅ i : s, f i = ⨅ (t : ι) (_ : t ∈ s), f t :=
  haveI : Nonempty s := Set.Nonempty.to_subtype hs
  ciInf_subtype hf hf'

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