comp_inf_eq_inf_comp_of_is_total — Mathlib

English

If g is monotone and preserves bottom, then g preserves infima: g(inf f) = inf (g ∘ f).

Русский

Если g монотонна и сохраняет ⊥, то она сохраняет инфимумы: g(inf f) = inf (g ∘ f).

LaTeX

$$$g(\inf f) = \inf (g \circ f)$, при монотонности g и $g(\bot) = \bot$$$

Lean4

theorem comp_inf_eq_inf_comp_of_is_total [SemilatticeInf β] [OrderTop β] (g : α → β) (mono_g : Monotone g)
    (top : g ⊤ = ⊤) : g (s.inf f) = s.inf (g ∘ f) :=
  comp_inf_eq_inf_comp g mono_g.map_inf top

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