Naming the strong Yosida exponential limit

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Semigroup_Yosida_Limit

noncomputable section
namespace FunctionalInequalities
namespace Analysis
namespace Semigroup
variable {H₀ H₁ : Type*} [NormedAddCommGroup H₀] [InnerProductSpace ℝ H₀] [CompleteSpace H₀]
  [NormedAddCommGroup H₁] [InnerProductSpace ℝ H₁] [CompleteSpace H₁]
namespace Generated
/-- `P_t f`: the strong limit of `exp (-t • L_s) f` as `s ↓ 0` for `t ≥ 0` (chosen from the adjoint-product identification), and
`f` for `t < 0`. Formally `exp (-t T†T) f`. -/
def apply (T : H₀ →ₗ.[ℝ] H₁) (hT : T.IsClosed) (hd : Dense (T.domain : Set H₀))
    (t : ℝ) (f : H₀) : H₀ :=
  if ht : 0 ≤ t then Classical.choose (exists_limit_exp_neg_smul_yosida T hT hd f ht) else f
/-- The defining property of `P_t f` for `t ≥ 0`: `exp (-t • L_s) f → P_t f` as `s ↓ 0`. -/
theorem yosida_limit (T : H₀ →ₗ.[ℝ] H₁) (hT : T.IsClosed) (hd : Dense (T.domain : Set H₀))
    {t : ℝ} (ht : 0 ≤ t) (f : H₀) {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ {s : ℝ} (hs : 0 < s), s < δ →
      ‖NormedSpace.exp (-t • yosida T hT hs) f - Generated.apply T hT hd t f‖ < ε := by
  unfold Generated.apply
  rw [dif_pos ht]
  exact Classical.choose_spec (exists_limit_exp_neg_smul_yosida T hT hd f ht) hε
end Generated
end Semigroup
end Analysis
end FunctionalInequalities