comp

Mathlib.Logic.Function.Defs

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

← MathLib Explorer

English

If g is bijective and f is bijective, then g ∘ f is bijective.

Русский

Если g и f биективны, то g ∘ f биективна.

LaTeX

$$$ \text{Bijective } g \Rightarrow \text{Bijective } f \Rightarrow \text{Bijective } (g \circ f) $$$

Lean4

theorem comp {g : β → φ} {f : α → β} : Bijective g → Bijective f → Bijective (g ∘ f)
  | ⟨h_ginj, h_gsurj⟩, ⟨h_finj, h_fsurj⟩ => ⟨h_ginj.comp h_finj, h_gsurj.comp h_fsurj⟩

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

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

Разделы

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

Аффилиация

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