stratum_eq_bot_iff

Mathlib.Algebra.Order.Module.HahnEmbedding

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

English

Each ArchimedeanStrata stratum is an Archimedean module.

Русский

Каждый слой ArchimedeanStrata является архимедовым модулем.

LaTeX

$$$ \text{Archimedean} (u.stratum\; c) $$$

Lean4

theorem stratum_eq_bot_iff : u.stratum c = ⊥ ↔ c = ⊤
    where
  mp h := by simpa [h] using u.ball_sup_stratum_eq c
  mpr := by rintro rfl; simp

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

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

Разделы

Аффилиация

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