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{IsMinFilter}(f,l,a) \rightarrow \text{IsMinFilter}(g,l,a) \rightarrow \text{IsMinFilter}(\lambda x.\, op(f x)(g x), l, a)$$$
Lean4
theorem bicomp_mono [Preorder δ] {op : β → γ → δ} (hop : ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) op op) (hf : IsMinFilter f l a)
{g : α → γ} (hg : IsMinFilter g l a) : IsMinFilter (fun x => op (f x) (g x)) l a :=
mem_of_superset (inter_mem hf hg) fun _x ⟨hfx, hgx⟩ => hop hfx hgx
