isConformalMap_of_subsingleton

Mathlib.Analysis.Normed.Operator.Conformal

URI: https://scilib.ai/kg/mathlib#isConformalMap_of_subsingleton

← MathLib Explorer

English

If M is a singleton, any linear map f' : M →L[R] N is conformal.

Русский

Если M состоит из одного элемента, любая линейная карта f' : M →L[R] N конформна.

LaTeX

$$$IsConformalMap f'$$$

Lean4

@[nontriviality]
theorem isConformalMap_of_subsingleton [Subsingleton M] (f' : M →L[R] N) : IsConformalMap f' :=
  ⟨1, one_ne_zero, ⟨0, fun x => by simp [Subsingleton.elim x 0]⟩, Subsingleton.elim _ _⟩

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

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

Разделы

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

Аффилиация

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