inv'_one

Mathlib.SetTheory.Game.Basic

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.inv'_one

← MathLib Explorer

English

inv' 1 has the same moves as 1; thus inv' 1 ≡ 1.

Русский

inv' 1 имеет те же ходы, что и 1; следовательно, inv' 1 эквивалентно 1.

LaTeX

$$$ inv' 1 \equiv 1 $$$

Lean4

/-- `inv' 1` has exactly the same moves as `1`. -/
theorem inv'_one : inv' 1 ≡ 1 := by
  rw [Identical.ext_iff]
  constructor
  · simp [memₗ_def, inv', isEmpty_subtype]
  · simp [memᵣ_def, inv', isEmpty_subtype]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru