archimedeanClassMk_of_mem_stratum

English

If a nonzero element a lies in the stratum corresponding to c, then ArchimedeanClass.mk a = c.

Русский

Если элемент a не равен нулю и принадлежит слою, соответствующему c, то ArchimedeanClass.mk a = c.

LaTeX

$$$ a \in u.stratum c \text{ и } a \neq 0 \Rightarrow \operatorname{ArchimedeanClass.mk} a = c $$$

Lean4

theorem archimedeanClassMk_of_mem_stratum {a : M} (ha : a ∈ u.stratum c) (h0 : a ≠ 0) : ArchimedeanClass.mk a = c :=
  by
  apply le_antisymm
  · have hc : c ≠ ⊤ := by
      contrapose! h0
      rw [u.stratum_eq_bot_iff.mpr h0] at ha
      simpa using ha
    contrapose! h0 with hlt
    have ha' : a ∈ ball K c := (mem_ball_iff K hc).mpr hlt
    exact (Submodule.disjoint_def.mp (u.disjoint_ball_stratum _)) _ ha' ha
  · apply (mem_closedBall_iff K).mp
    rw [← u.ball_sup_stratum_eq c]
    exact Submodule.mem_sup_right ha

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