stratum_top

Mathlib.Algebra.Order.Module.HahnEmbedding

URI: https://scilib.ai/kg/mathlib#HahnEmbedding.ArchimedeanStrata.stratum_top

English

For any ArchimedeanStrata, the top stratum equals the bottom submodule.

Русский

Для любой ArchimedeanStrata верхний слой равен нулевому подмодулю.

LaTeX

$$$ u.stratum(\top) = ⊥ $$$

Lean4

@[simp]
theorem stratum_top : u.stratum (⊤ : ArchimedeanClass M) = ⊥ := by simpa using u.ball_sup_stratum_eq ⊤

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

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

Разделы

Аффилиация

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