infinite

Mathlib.Analysis.Normed.Module.Basic

URI: https://scilib.ai/kg/mathlib#NontriviallyNormedField.infinite

English

A nontrivially normed field 𝕜 is infinite.

Русский

Ненулевое нормированное поле 𝕜 бесконечно по множеству элементов.

LaTeX

$$$|\mathbb{K}| = \\infty$$$

Lean4

instance (priority := 80) infinite : Infinite 𝕜 :=
  ⟨fun _ ↦ NormedSpace.unbounded_univ 𝕜 𝕜 (Set.toFinite _).isBounded⟩

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

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

Разделы

Аффилиация

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