iSupLift_of_mem

Mathlib.Algebra.Star.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalStarSubalgebra.iSupLift_of_mem

← MathLib Explorer

English

iSupLift_mk: for i, x ∈ K_i and hx ∈ T, iSupLift K dir f hf T hT ⟨x, hx⟩ = f i x.

Русский

iSupLift_mk: для i и x ∈ K_i, hx ∈ T, iSupLift(K,dir,f,hf,T,hT)(⟨x,hx⟩) = f_i x.

LaTeX

$$$iSupLift\\ K dir f hf T hT \\langle x, hx \\rangle = f i x$$$

Lean4

theorem iSupLift_of_mem {i : ι} (x : T) (hx : (x : A) ∈ K i) : iSupLift K dir f hf T hT x = f i ⟨x, hx⟩ :=
  by
  subst hT
  dsimp [iSupLift]
  apply Set.iUnionLift_of_mem

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

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

Разделы

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

Аффилиация

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