instNonempty — Mathlib

English

There exists at least one ArchimedeanStrata K M, i.e., the collection of archimedean strata is nonempty.

Русский

Существует по крайней мере одна ArchimedeanStrata K M, то есть множество слоёв архимедов непусто.

LaTeX

$$$ \exists u:\ ArchimedeanStrata\ K\ M, True $$$

Lean4

instance : Nonempty (ArchimedeanStrata K M) :=
  by
  have hstratum (c : ArchimedeanClass M) : ∃ G : Submodule K M, Disjoint (ball K c) G ∧ ball K c ⊔ G = closedBall K c :=
    IsModularLattice.exists_disjoint_and_sup_eq <| ball_le_closedBall _
  choose g h1 h2 using hstratum
  exact ⟨g, h1, h2⟩

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