subsingleton_h1Cotangent — Mathlib

English

If S is IsStandardSmooth, the subsingleton property of H1Cotangent persists.

Русский

Если S является IsStandardSmooth, свойство subsingleton для H1Cotangent сохраняется.

LaTeX

$$instance subsingleton_h1Cotangent : Subsingleton H1Cotangent$$

Lean4

instance subsingleton_h1Cotangent [IsStandardSmooth R S] : Subsingleton (H1Cotangent R S) :=
  by
  obtain ⟨_, _, _, _, ⟨P⟩⟩ := ‹IsStandardSmooth R S›
  exact P.equivH1Cotangent.symm.toEquiv.subsingleton

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