iInf_congr — Mathlib

English

Let e: ι ≃ ι' and suppose g(e(x)) = f(x) for all x. Then the infimum of f over x equals the infimum of g over y.

Русский

Пусть e: ι ≃ ι' и для всех x выполнено g(e(x)) = f(x). Тогда инфиму́мум f по x равен инфиму́муму g по y.

LaTeX

$$$$\\inf_{x} f(x) = \\inf_{y} g(y)\\quad\\text{if } g(e(x)) = f(x) \\text{ for all } x.$$$$

Lean4

protected theorem iInf_congr {g : ι' → α} (h : ι → ι') (h1 : Surjective h) (h2 : ∀ x, g (h x) = f x) :
    ⨅ x, f x = ⨅ y, g y :=
  @Function.Surjective.iSup_congr αᵒᵈ _ _ _ _ _ h h1 h2

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