prodMap

Mathlib.Data.Prod.Basic

URI: https://scilib.ai/kg/mathlib#Function.Bijective.prodMap

English

If f and g are injective, then Prod.map f g is injective.

Русский

Если f и g инъективны, то Prod.map f g инъективен.

LaTeX

$$Injective (Prod.map f g)$$

Lean4

theorem prodMap (hf : Bijective f) (hg : Bijective g) : Bijective (map f g) :=
  ⟨hf.1.prodMap hg.1, hf.2.prodMap hg.2⟩

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

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

Разделы

Аффилиация

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