add — Mathlib

English

If f and g are both minimal with respect to l at a, then their sum f + g is also minimal at a with respect to l.

Русский

Если f и g оба минимальны относительно l в точке a, то их сумма f + g также минимальна относительно l в точке a.

LaTeX

$$$hf : IsMinFilter f l a \;\; hg : IsMinFilter g l a \Rightarrow IsMinFilter (\lambda x. f x + g x) l a$$$

Lean4

theorem add (hf : IsMinFilter f l a) (hg : IsMinFilter g l a) : IsMinFilter (fun x => f x + g x) l a :=
  show IsMinFilter (fun x => f x + g x) l a from hf.bicomp_mono (fun _x _x' hx _y _y' hy => add_le_add hx hy) hg

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