iInf_congr — Mathlib

English

If e: ι ≃ ι' and g is as above with h: ∀ x, g(e(x)) = f(x), then the infimum over x of g(e(x)) equals the infimum over y of g(y).

Русский

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

LaTeX

$$$$\\inf_{x} g(e(x)) = \\inf_{y} g(y).$$$$

Lean4

protected theorem iInf_congr {g : ι' → α} (e : ι ≃ ι') (h : ∀ x, g (e x) = f x) : ⨅ x, f x = ⨅ y, g y :=
  @Equiv.iSup_congr αᵒᵈ _ _ _ _ _ e h

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