iSup_image — Mathlib

English

For γ, f: β → γ, g: γ → α, and t ⊆ β, the supremum over c ∈ f''t of g c equals the supremum over b ∈ t of g(f b).

Русский

Для γ, f: β → γ, g: γ → α и t ⊆ β, супремум по c ∈ f''t g(c) равен супремуму по b ∈ t g(f(b)).

LaTeX

$$$$ \\sup_{c \\in f''t} g(c) = \\sup_{b \\in t} g(f(b)) $$$$

Lean4

theorem iSup_image {γ} {f : β → γ} {g : γ → α} {t : Set β} : ⨆ c ∈ f '' t, g c = ⨆ b ∈ t, g (f b) := by
  rw [← sSup_image, ← sSup_image, ← image_comp, comp_def]

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