comp_partialSups — Mathlib

English

The partialSups operator commutes with composition: partialSups (g ∘ f) = g ∘ partialSups f.

Русский

Операция partialSups коммутирует с композицией: partialSups (g ∘ f) = g ∘ partialSups f.

LaTeX

$$$\\mathrm{partialSups}(\\,\\circ\\,(g) \\,\\circ f) = g \\circ \\mathrm{partialSups} f$$$

Lean4

theorem comp_partialSups {F : Type*} [FunLike F α β] [SupHomClass F α β] (f : ι → α) (g : F) :
    partialSups (g ∘ f) = g ∘ partialSups f := by funext _; simp [partialSups]

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