fuzzy_zero_iff_lf — Mathlib

English

Let G be an impartial game. Then G is fuzzy with 0 if and only if G is left-fuzzy with respect to 0, i.e. G ∥ 0 ⇔ G ⧏ 0.

Русский

Пусть G — непредвзятая игра. Тогда G размыт по отношению к нулю тогда, когда G слева относится к 0 (G ∥ 0 ⇔ G ⧏ 0).

LaTeX

$$$ [\text{Impartial}(G)] \rightarrow \bigl( G \parallel 0 \iff G \⧏ 0 \bigr) $$$

Lean4

theorem fuzzy_zero_iff_lf : G ‖ 0 ↔ G ⧏ 0 :=
  ⟨And.left, fun h => ⟨h, lf_zero_iff.1 h⟩⟩

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