iSup_finset_image — Mathlib

English

For f: γ → α, g: α → β and s: Finset γ, the supremum over the image of s equals the supremum 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 \\sup_{x \\in s^{\\mathrm{image} f}} g(x) = \\sup_{y \\in s} g(f(y)). $$$$

Lean4

theorem iSup_finset_image {f : γ → α} {g : α → β} {s : Finset γ} : ⨆ x ∈ s.image f, g x = ⨆ y ∈ s, g (f y) := by
  rw [← iSup_coe, coe_image, iSup_image, iSup_coe]

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