add

Mathlib.Algebra.Group.EvenFunction

URI: https://scilib.ai/kg/mathlib#Function.Even.add

English

If f and g are even, then f + g is even.

Русский

Если функции f и g чётны, то их сумма чётна.

LaTeX

$$Even f ∧ Even g ⇒ Even (f + g)$$

Lean4

theorem add [Add β] {f g : α → β} (hf : f.Even) (hg : g.Even) : (f + g).Even :=
  by
  intro a
  simp only [hf a, hg a, Pi.add_apply]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru