nim_fuzzy_zero_of_ne_zero — Mathlib

English

If o is nonzero, Nim(o) is fuzzy with 0; i.e., Nim(o) is incomparable with 0 in the fuzzy sense.

Русский

Если o ≠ 0, Nim(o) неразложим по отношению к 0; Nim(o) является неразделимым с 0 в неразложимой мере.

LaTeX

$$$ \text{If } o \neq 0,\; \mathrm{nim}(o) \;\mathbin{\|\!\!\!\|} \; 0. $$$

Lean4

theorem nim_fuzzy_zero_of_ne_zero {o : Ordinal} (ho : o ≠ 0) : nim o ‖ 0 :=
  by
  rw [Impartial.fuzzy_zero_iff_lf, lf_zero_le]
  use toRightMovesNim ⟨0, Ordinal.pos_iff_ne_zero.2 ho⟩
  simp

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