iInf_subtype'' — Mathlib

English

For a predicate p on ι and f : ι → α with f i h depending on h : p i, the infimum over i : s with h of f i h equals the infimum over x : Subtype p of f x x.property.

Русский

Для предиката p на ι и функции f(i,h) с зависимостью от h: p(i) инфимум по i с доказательством p(i) равен инфимуму по элементам подпредельного множества.

LaTeX

$$$ \\inf_{i : s} f(i) = \\inf_{t : ι} (t \\in s) \\inf_{x: t \\in s} f(t) $$$

Lean4

theorem iInf_subtype'' {ι} (s : Set ι) (f : ι → α) : ⨅ i : s, f i = ⨅ (t : ι) (_ : t ∈ s), f t :=
  iInf_subtype

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