add — Mathlib

English

If f and g are both maximal with respect to l at a, then f + g is maximal at a with respect to l.

Русский

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

LaTeX

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

Lean4

theorem add (hf : IsMaxFilter f l a) (hg : IsMaxFilter g l a) : IsMaxFilter (fun x => f x + g x) l a :=
  show IsMaxFilter (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

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