map_involutive

Mathlib.Data.Prod.Basic

URI: https://scilib.ai/kg/mathlib#Prod.map_involutive

← MathLib Explorer

English

Involutive (Prod.map f g) iff Involutive f and Involutive g.

Русский

Инволютивность Prod.map эквивалентна инволютивности f и g.

LaTeX

$$Iff (Involutive (Prod.map f g)) (And (Involutive f) (Involutive g))$$

Lean4

@[simp]
theorem map_involutive [Nonempty α] [Nonempty β] {f : α → α} {g : β → β} :
    Involutive (map f g) ↔ Involutive f ∧ Involutive g :=
  map_leftInverse

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

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

Разделы

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

Аффилиация

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