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