iInf_image — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem iInf_image : ∀ {γ} {f : β → γ} {g : γ → α} {t : Set β}, ⨅ c ∈ f '' t, g c = ⨅ b ∈ t, g (f b) :=
  @iSup_image αᵒᵈ _ _

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