add — Mathlib

English

If f and g are CircleIntegrable with the same center and radius, then f + g is CircleIntegrable.

Русский

Если f и g CircleIntegrable с одинаковым центром и радиусом, то f + g CircleIntegrable.

LaTeX

$$$\text{CircleIntegrable}(f,c,R) \;\land \; \text{CircleIntegrable}(g,c,R) \Rightarrow \text{CircleIntegrable}(f+g,c,R).$$$

Lean4

nonrec theorem add (hf : CircleIntegrable f c R) (hg : CircleIntegrable g c R) : CircleIntegrable (f + g) c R :=
  hf.add hg

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