Theorems · Definition · order theory

HahnEmbedding.IsPartial.casesOn

{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] →
                      {R : Type u_3} →
                        [inst_9 : AddCommGroup R] →
                          [inst_10 : LinearOrder R] →
                            [inst_11 : Module K R] →
                              {seed : HahnEmbedding.Seed K M R} →
                                {f : M →ₗ.[K] Lex (HahnSeries (FiniteArchimedeanClass M) R)} →
                                  {motive : HahnEmbedding.IsPartial seed f → Sort u} →
                                    (t : HahnEmbedding.IsPartial seed f) →
                                      ((strictMono : StrictMono ↑f) →
                                          (baseEmbedding_le : seed.baseEmbedding ≤ f) →
                                            (truncLT_mem_range :
                                                ∀ (x : ↥f.domain) (c : FiniteArchimedeanClass M),
                                                  toLex ((HahnSeries.truncLTLinearMap K c) (ofLex (↑f x))) ∈
                                                    f.toFun.range) →
                                              motive ⋯) →
                                        motive t

Defined in

Mathlib.Algebra.Order.Module.HahnEmbedding

Cited by

0 results in Mathlib

Foundations

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

Assumes

DivisionRingLinearOrderIsOrderedRingArchimedeanAddCommGroupLinearOrderIsOrderedAddMonoidModuleIsOrderedModuleAddCommGroupLinearOrderModule