invFun

Mathlib.LinearAlgebra.Quotient.Pi

URI: https://scilib.ai/kg/mathlib#Submodule.quotientPi_aux.invFun

Lean4

@[simp]
def invFun : (∀ i, Ms i ⧸ p i) → (∀ i, Ms i) ⧸ pi Set.univ p :=
  piQuotientLift p (pi Set.univ p) _ fun _ => le_comap_single_pi p

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

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

Разделы

Аффилиация

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