comp_inf_eq_inf_comp — Mathlib

English

If g: α → γ preserves inf (g(x ⊓ y) = g(x) ⊓ g(y)) and maps top to top, then g(s.inf f) = s.inf (g ∘ f) for Finset s.

Русский

Если отображение g сохраняет инфимум (g(x ⊓ y) = g(x) ⊓ g(y)) и отображает верхнюю границу в верхнюю границу, то $ g(\inf_{b∈s} f(b)) = \inf_{b∈s} g(f(b)) $.

LaTeX

$$$ g( s.\\inf f ) = s.\\inf (g \\circ f) $$$

Lean4

theorem comp_inf_eq_inf_comp [SemilatticeInf γ] [OrderTop γ] {s : Finset β} {f : β → α} (g : α → γ)
    (g_inf : ∀ x y, g (x ⊓ y) = g x ⊓ g y) (top : g ⊤ = ⊤) : g (s.inf f) = s.inf (g ∘ f) :=
  @comp_sup_eq_sup_comp αᵒᵈ _ γᵒᵈ _ _ _ _ _ _ _ g_inf top

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