Theorems · Definition · order theory

HahnEmbedding.ArchimedeanStrata.recOn

{K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      {motive : HahnEmbedding.ArchimedeanStrata K M → Sort u} →
                        (t : HahnEmbedding.ArchimedeanStrata K M) →
                          ((stratum : FiniteArchimedeanClass M → Submodule K M) →
                              (disjoint_ball_stratum :
                                  ∀ (c : FiniteArchimedeanClass M),
                                    Disjoint (FiniteArchimedeanClass.ball K c) (stratum c)) →
                                (ball_sup_stratum_eq :
                                    ∀ (c : FiniteArchimedeanClass M),
                                      FiniteArchimedeanClass.ball K c ⊔ stratum c =
                                        FiniteArchimedeanClass.closedBall K c) →
                                  motive
                                    { stratum := stratum, disjoint_ball_stratum := disjoint_ball_stratum,
                                      ball_sup_stratum_eq := ball_sup_stratum_eq }) →
                            motive t

Defined in

Mathlib.Algebra.Order.Module.HahnEmbedding

Cited by

0 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionRingLinearOrderIsOrderedRingArchimedeanAddCommGroupLinearOrderIsOrderedAddMonoidModuleIsOrderedModule