biInf_comp — Mathlib

English

Under an equivalence e, the infimum over i ∈ e.symm'' s of g(e i) equals the infimum over i ∈ s of g i.

Русский

С сохранением эквивалентности, инфимум над i∈e.symm''s g(e i) равен инфимуму над i∈s g i.

LaTeX

$$$ \\inf_{i \\in e.symm '' s} g(e(i)) = \\inf_{i \\in s} g(i). $$$

Lean4

theorem biInf_comp {ι ι' : Type*} {g : ι' → α} (e : ι ≃ ι') (s : Set ι') : ⨅ i ∈ e.symm '' s, g (e i) = ⨅ i ∈ s, g i :=
  e.biSup_comp s (α := αᵒᵈ)

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