nfp_mul_eq_opow_omega0 — Mathlib

English

If a · b = b, then either b = 0 or a^ω ≤ b.

Русский

Если a · b = b, то либо b = 0, либо a^ω ≤ b.

LaTeX

$$$$ a \cdot b = b \Rightarrow (b = 0) \lor (a^{\omega} \le b) $$$$

Lean4

theorem nfp_mul_eq_opow_omega0 {a b : Ordinal} (hb : 0 < b) (hba : b ≤ a ^ ω) : nfp (a * ·) b = a ^ ω :=
  by
  rcases eq_zero_or_pos a with ha | ha
  · rw [ha, zero_opow omega0_ne_zero] at hba ⊢
    simp_rw [Ordinal.le_zero.1 hba, zero_mul]
    exact nfp_zero_left 0
  apply le_antisymm
  · apply nfp_le_fp (isNormal_mul_right ha).monotone hba
    rw [← opow_one_add, one_add_omega0]
  rw [← nfp_mul_one ha]
  exact nfp_monotone (isNormal_mul_right ha).monotone (one_le_iff_pos.2 hb)

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