left_comp

Mathlib.Algebra.Group.EvenFunction

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

← MathLib Explorer

English

If g is even and f is any function, then f ∘ g is even.

Русский

Если g чётна, а f произвольна, то композиция f ∘ g чётна.

LaTeX

$$Even(f ∘ g)$$

Lean4

/-- If `f` is arbitrary and `g` is even, then `f ∘ g` is even. -/
theorem left_comp {g : α → β} (hg : g.Even) (f : β → γ) : (f ∘ g).Even :=
  (congr_arg f <| hg ·)

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

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

Разделы

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

Аффилиация

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