fuzzy_zero_iff_gf — Mathlib

English

Let G be an impartial game. Then G is fuzzy with 0 if and only if G.Fuzzy 0 holds, i.e., G ∥ 0 ⇔ G.Fuzzy 0.

Русский

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

LaTeX

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

Lean4

theorem fuzzy_zero_iff_gf : G ‖ 0 ↔ 0 ⧏ G :=
  ⟨And.right, fun h => ⟨lf_zero_iff.2 h, h⟩⟩

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