preOmega_natCast — Mathlib

English

For every natural number n, preOmega(n) = n.

Русский

Для каждого натурального числа n выполняется preOmega(n) = n.

LaTeX

$$$\forall n \in \mathbb{N},\ \mathrm{preOmega}(n) = n$$$

Lean4

@[simp]
theorem preOmega_natCast (n : ℕ) : preOmega n = n := by
  induction n with
  | zero => exact preOmega_zero
  | succ n IH =>
    apply (le_preOmega_self _).antisymm'
    apply enumOrd_succ_le not_bddAbove_isInitial (isInitial_natCast _) (IH.trans_lt _)
    rw [Nat.cast_lt]
    exact lt_succ n

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