comp_odd

Mathlib.Algebra.Group.EvenFunction

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

← MathLib Explorer

English

If f is even and g is odd, then f ∘ g is even.

Русский

Если f чётна, а g нечётна, тогда f ∘ g чётна.

LaTeX

$$Even(f ∘ g)$$

Lean4

/-- If `f` is even and `g` is odd, then `f ∘ g` is even. -/
theorem comp_odd [Neg β] {f : β → γ} (hf : f.Even) {g : α → β} (hg : g.Odd) : (f ∘ g).Even :=
  by
  intro a
  simp only [comp_apply, hg a, hf _]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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