sub_nfBelow — Mathlib

English

For o1,o2,b, if o1.NFBelow b and o2.NF then (o1 - o2).NFBelow b.

Русский

Для o1, o2, b, если o1.NFBelow b и o2.NF, то (o1 - o2).NFBelow b.

LaTeX

$$$\forall {o_1 o_2 : ONote} {b : Ordinal},\; o_1.NFBelow b \rightarrow o_2.NF \rightarrow (instHSub.hSub o_1 o_2).NFBelow b$$$

Lean4

theorem sub_nfBelow : ∀ {o₁ o₂ b}, NFBelow o₁ b → NF o₂ → NFBelow (o₁ - o₂) b
  | 0, o, b, _, h₂ => by cases o <;> exact NFBelow.zero
  | oadd _ _ _, 0, _, h₁, _ => h₁
  | oadd e₁ n₁ a₁, oadd e₂ n₂ a₂, b, h₁, h₂ =>
    by
    have h' := sub_nfBelow h₁.snd h₂.snd
    simp only [HSub.hSub, Sub.sub, sub] at h' ⊢
    have := @cmp_compares _ _ h₁.fst h₂.fst
    cases h : cmp e₁ e₂
    · apply NFBelow.zero
    · rw [Nat.sub_eq]
      simp only [h, Ordering.compares_eq] at this
      subst e₂
      cases (n₁ : ℕ) - n₂
      · by_cases en : n₁ = n₂ <;> simp only [en, ↓reduceIte]
        · exact h'.mono (le_of_lt h₁.lt)
        · exact NFBelow.zero
      · exact NFBelow.oadd h₁.fst h₁.snd h₁.lt
    · exact h₁

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