piMap

Mathlib.Logic.Function.Basic

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

← MathLib Explorer

English

If each f_i is Bijective, then Pi.map f is Bijective.

Русский

Если каждый f_i биективна, то Pi.map f биективна.

LaTeX

$$$ \forall i, \text{Bijective}(f_i) \rightarrow \text{Bijective}(\mathrm{Pi.map} f) $$$

Lean4

theorem piMap {ι : Sort*} {α β : ι → Sort*} {f : ∀ i, α i → β i} (hf : ∀ i, Bijective (f i)) : Bijective (Pi.map f) :=
  ⟨.piMap fun i ↦ (hf i).1, .piMap fun i ↦ (hf i).2⟩

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

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

Разделы

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

Аффилиация

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