exists_lt_add_of_not_principal_add

English

If an ordinal a is not principal for addition, then a can be decomposed as b + c with b < a and c < a.

Русский

Если ординал a не является принципиальным для сложения, то он может быть разложен в виде b + c, где b < a и c < a.

LaTeX

$$$\neg Principal(\cdot + \cdot, a) \Rightarrow \exists b

Lean4

theorem exists_lt_add_of_not_principal_add (ha : ¬Principal (· + ·) a) : ∃ b < a, ∃ c < a, b + c = a :=
  by
  rw [not_principal_iff] at ha
  rcases ha with ⟨b, hb, c, hc, H⟩
  refine ⟨b, hb, _, lt_of_le_of_ne (sub_le_self a b) fun hab => ?_, Ordinal.add_sub_cancel_of_le hb.le⟩
  rw [← sub_le, hab] at H
  exact H.not_gt hc

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