range_eq_univ_of_not_isRCLikeNormedField

Mathlib.Geometry.Manifold.IsManifold.Basic

URI: https://scilib.ai/kg/mathlib#ModelWithCorners.range_eq_univ_of_not_isRCLikeNormedField

English

If 𝕜 is not RC-like, then range I = univ.

Русский

Если 𝕜 не RC-подобно, то диапазон I равен всему пространству.

LaTeX

$$$ \\neg \\mathrm{IsRCLikeNormedField}(\\,\\, 𝕜) \\Rightarrow \\mathrm{range}(I) = \\mathrm{univ} $$$

Lean4

theorem range_eq_univ_of_not_isRCLikeNormedField (h : ¬IsRCLikeNormedField 𝕜) : range I = univ := by
  simpa [h] using I.convex_range'

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

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

Разделы

Аффилиация

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