iInf_comp — Mathlib

English

Let α be a complete lattice, and let f: ι → ι' be a surjective map, with g: ι' → α. Then the infimum of g ∘ f over x equals the infimum of g over y.

Русский

Пусть α — полная решетка, f: ι → ι' сюръективно, и g: ι' → α. Тогда инфиму́мум (g ∘ f)(x) по x равен инфиму́муму g(y) по y.

LaTeX

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

Lean4

theorem iInf_comp {f : ι → ι'} (hf : Surjective f) (g : ι' → α) : ⨅ x, g (f x) = ⨅ y, g y :=
  @Function.Surjective.iSup_comp αᵒᵈ _ _ _ f hf g

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