adjoint_apply_of_dense

Mathlib.Analysis.InnerProductSpace.LinearPMap

URI: https://scilib.ai/kg/mathlib#LinearPMap.adjoint_apply_of_dense

← MathLib Explorer

English

If T.domain is dense, then T† y = adjointAux hT y for y ∈ T†.domain.

Русский

Если область определения T плотна, то T† y = adjointAux hT y для y ∈ T†.domain.

LaTeX

$$T† y = adjointAux hT y$$

Lean4

theorem adjoint_apply_of_dense (y : T†.domain) : T† y = adjointAux hT y := by
  classical
  change (if hT : Dense (T.domain : Set E) then adjointAux hT else 0) y = _
  simp only [hT, dif_pos]

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

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

Разделы

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

Аффилиация

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