forall_rightMoves_fuzzy_iff_equiv_zero

English

For an impartial G, G.moveRight j is fuzzy with 0 for all j if and only if G ≈ 0.

Русский

Для непредвзятой G переходы вправо G.moveRight j размыт по отношению к 0 для всех j тогда и только тогда, когда G ≈ 0.

LaTeX

$$$ [\text{Impartial}(G)] \rightarrow \bigl( \forall j, G.moveRight(j) \parallel 0 \bigr) \iff (G \approx 0) $$$

Lean4

theorem forall_rightMoves_fuzzy_iff_equiv_zero : (∀ j, G.moveRight j ‖ 0) ↔ G ≈ 0 :=
  by
  refine ⟨fun hb => ?_, fun hp i => ?_⟩
  · rw [equiv_zero_iff_ge G, zero_le_lf]
    exact fun i => (hb i).2
  · rw [fuzzy_zero_iff_gf]
    exact hp.2.lf_moveRight i

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