mem_adjoint_domain_iff — Mathlib

English

If there exists w ∈ E such that ∀ x ∈ T.domain, ⟪w, x⟫ = ⟪y, T x⟫, then y ∈ T†.domain.

Русский

Если существует w ∈ E такое, что для всех x ∈ T.domain выполняется ⟪w, x⟫ = ⟪y, T x⟫, то y ∈ T†.domain.

LaTeX

$$If ∃ w ∈ E, ∀ x ∈ T.domain, ⟪w, x⟫ = ⟪y, T x⟫ then y ∈ T†.domain$$

Lean4

theorem mem_adjoint_domain_iff (y : F) : y ∈ T†.domain ↔ Continuous ((innerₛₗ 𝕜 y).comp T.toFun) :=
  Iff.rfl

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