nf_repr_split' — Mathlib

English

For NF o and split'(o) = (o', m), we have NF o' and repr(o) = ω·repr(o') + m; i.e., the representation of o decomposes along the split.

Русский

Для NF о и split'(о) = (о', m) выполняется NF(о') и repr(о) = ω·repr(о') + m; т.е. представление o разлагается по разбиению.

LaTeX

$$$\forall {o\,o'\,m} [o.NF],\; split'(o) = (o',m) \rightarrow (\; o'.NF \land \mathrm{repr}(o) = \omega \cdot \mathrm{repr}(o') + m\;)$$$

Lean4

theorem nf_repr_split' : ∀ {o o' m} [NF o], split' o = (o', m) → NF o' ∧ repr o = ω * repr o' + m
  | 0, o', m, _, p => by injection p; substs o' m; simp [NF.zero]
  | oadd e n a, o', m, h, p =>
    by
    by_cases e0 : e = 0 <;>
      simp only [split', e0, ↓reduceIte, Prod.mk.injEq, repr, repr_zero, opow_zero, one_mul] at p ⊢
    · rcases p with ⟨rfl, rfl⟩
      simp [h.zero_of_zero e0, NF.zero]
    · revert p
      rcases h' : split' a with ⟨a', m'⟩
      haveI := h.fst
      haveI := h.snd
      obtain ⟨IH₁, IH₂⟩ := nf_repr_split' h'
      simp only [IH₂, and_imp]
      intros
      substs o' m
      have : (ω : Ordinal.{0}) ^ repr e = ω ^ (1 : Ordinal.{0}) * ω ^ (repr e - 1) :=
        by
        have := mt repr_inj.1 e0
        rw [← opow_add, Ordinal.add_sub_cancel_of_le (one_le_iff_ne_zero.2 this)]
      refine ⟨NF.oadd (by infer_instance) _ ?_, ?_⟩
      · simp only [opow_one, repr_sub, repr_one, Nat.cast_one] at this ⊢
        refine IH₁.below_of_lt' <| (mul_lt_mul_iff_right₀ omega0_pos).1 <| lt_of_le_of_lt (le_add_right _ m') ?_
        rw [← this, ← IH₂]
        exact h.snd'.repr_lt
      · rw [this]
        simp [mul_add, mul_assoc, add_assoc]

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