iInf_ne_top_subtype — Mathlib

English

When taking the infimum of f : ι → α, removing those i for which f(i) = ⊤ does not change the result: iInf f = iInf { i // f(i) ≠ ⊤ } f(i).

Русский

При взятии инфимума от f: ι → α удаление индексов, на которых f(i) = ⊤, не меняет результат: iInf f = iInf { i | f(i) ≠ ⊤ } f(i).

LaTeX

$$$\\displaystyle \\inf_{i} f(i) = \\inf_{i:\\, f(i) \\neq \\top} f(i)$$$

Lean4

/-- When taking the infimum of `f : ι → α`, the elements of `ι` on which `f` gives `⊤` can be
dropped, without changing the result. -/
theorem iInf_ne_top_subtype (f : ι → α) : ⨅ i : { i // f i ≠ ⊤ }, f i = ⨅ i, f i :=
  @iSup_ne_bot_subtype αᵒᵈ ι _ f

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