principal_add_iff_add_left_eq_self

English

For an ordinal o, Principal (· + ·) o holds if and only if for all a < o, a + o = o.

Русский

Для ординала o справедливо, что o является принципиальным для сложения, тогда и только тогда, когда для всех a < o выполняется a + o = o.

LaTeX

$$$Principal(\cdot + \cdot, o) \iff \forall a < o, a + o = o.$$$

Lean4

theorem principal_add_iff_add_left_eq_self : Principal (· + ·) o ↔ ∀ a < o, a + o = o :=
  by
  refine ⟨fun ho a hao => ?_, fun h a b hao hbo => ?_⟩
  · rcases lt_or_ge 1 o with ho₁ | ho₁
    · exact op_eq_self_of_principal hao (isNormal_add_right a) ho (isSuccLimit_of_principal_add ho₁ ho)
    · rcases le_one_iff.1 ho₁ with (rfl | rfl)
      · exact (Ordinal.not_lt_zero a hao).elim
      · rw [lt_one_iff_zero] at hao
        rw [hao, zero_add]
  · rw [← h a hao]
    exact (isNormal_add_right a).strictMono hbo

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