exists_right_move_equiv_iff_fuzzy_zero

English

An impartial G is fuzzy with 0 iff there exists a right move j with G.moveRight j equivalent to 0.

Русский

Неравномерность G по отношению к нулю эквивалентна существованию правого хода j, для которого G.moveRight j эквивалентно 0.

LaTeX

$$$ \bigl( \exists j, G.moveRight(j) \approx 0 \bigr) \iff (G \parallel 0) $$$

Lean4

theorem exists_right_move_equiv_iff_fuzzy_zero : (∃ j, G.moveRight j ≈ 0) ↔ G ‖ 0 :=
  by
  refine ⟨fun ⟨i, hi⟩ => (fuzzy_zero_iff_lf G).2 (lf_of_moveRight_le hi.1), fun hn => ?_⟩
  rw [fuzzy_zero_iff_lf G, lf_zero_le] at hn
  obtain ⟨i, hi⟩ := hn
  exact ⟨i, (equiv_zero_iff_le _).2 hi⟩

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