Documentation

InfinitaryLogic.Methods.HighlyTransitiveField

Linear ordered fields are highly order-transitive (issue #11 unit 6a) #

Every linear ordered field is a highly order-transitive linear order (HighlyOrderTransitive.of_field): a finite increasing tuple is moved onto another one point at a time, left to right — the first point by translation, and each subsequent point by a cut dilation (dilateAbove): the order automorphism that is the identity on (-∞, a] and the positive affine dilation z ↦ a + ((y-a)/(x-a)) * (z-a) above the last already-placed target a, carrying the current point x to its target y while fixing everything already placed.

The automorphism is built as a piecewise strictly monotone surjection (StrictMono.orderIsoOfSurjective) — no order-sum gluing needed.

source
def FirstOrder.dilateFun {K : Type u_1} [Field K] [LinearOrder K] (a c z : K) :
K

The cut-dilation function: identity up to a, positive dilation with factor c above.

Equations
Instances For
    source
    theorem FirstOrder.dilateFun_strictMono {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {a c : K} (hc : 0 < c) :
    StrictMono (dilateFun a c)
    source
    theorem FirstOrder.dilateFun_surjective {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {a c : K} (hc : 0 < c) :
    Function.Surjective (dilateFun a c)
    source
    noncomputable def FirstOrder.dilateAbove {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (a x y : K) (hx : a < x) (hy : a < y) :
    K ≃o K

    The cut dilation: the order automorphism that is the identity on (-∞, a] and carries x to y above a.

    Equations
    Instances For
      source
      theorem FirstOrder.dilateAbove_apply_of_le {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {a x y : K} (hx : a < x) (hy : a < y) {z : K} (hz : z ≤ a) :
      (dilateAbove a x y hx hy) z = z
      source
      theorem FirstOrder.dilateAbove_apply_point {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {a x y : K} (hx : a < x) (hy : a < y) :
      (dilateAbove a x y hx hy) x = y
      source
      theorem FirstOrder.HighlyOrderTransitive.of_field (K : Type u_2) [Field K] [LinearOrder K] [IsStrictOrderedRing K] :
      HighlyOrderTransitive K

      Every linear ordered field is highly order-transitive — the left-to-right point-moving induction: translation for the first point, cut dilations for the rest.