iInf_finset_image — Mathlib

English

For f: γ → α, g: α → β and s: Finset γ, the infimum over the image equals the infimum over s of g(f(y)): ⨅ x ∈ s.image f, g x = ⨅ y ∈ s, g (f y).

Русский

Для f: γ → α, g: α → β и s: Finset γ верно: ⨅ x ∈ s.image f, g x = ⨅ y ∈ s, g (f y).

LaTeX

$$$$\\displaystyle \\inf_{x \\in s^{\\mathrm{image} f}} g(x) = \\inf_{y \\in s} g(f(y)). $$$$

Lean4

theorem iInf_finset_image {f : γ → α} {g : α → β} {s : Finset γ} : ⨅ x ∈ s.image f, g x = ⨅ y ∈ s, g (f y) := by
  rw [← iInf_coe, coe_image, iInf_image, iInf_coe]

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