mem_adjoint_domain_of_exists — 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

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

Lean4

theorem mem_adjoint_domain_of_exists (y : F) (h : ∃ w : E, ∀ x : T.domain, ⟪w, x⟫ = ⟪y, T x⟫) : y ∈ T†.domain :=
  by
  obtain ⟨w, hw⟩ := h
  rw [T.mem_adjoint_domain_iff]
  have : Continuous ((innerSL 𝕜 w).comp T.domain.subtypeL) := by fun_prop
  convert this using 1
  exact funext fun x => (hw x).symm

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