bicomp_mono — Mathlib

English

If f and g are both minimal with respect to a, and op is a monotone operation on deltas, then op(f,g) is minimal with respect to a.

Русский

Если f и g минимальны относительно a, и операция op монотонна, тогда op(f,g) минимальна относительно a.

LaTeX

$$$\text{IsMinOn}(f,s,a) \rightarrow \text{IsMinOn}(g,s,a) \rightarrow \text{IsMinOn}(\lambda x.\, op(f x)(g x), s, a)$$$

Lean4

theorem bicomp_mono [Preorder δ] {op : β → γ → δ} (hop : ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) op op) (hf : IsMinOn f s a)
    {g : α → γ} (hg : IsMinOn g s a) : IsMinOn (fun x => op (f x) (g x)) s a :=
  IsMinFilter.bicomp_mono hop hf hg

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