subsingleton_short — Mathlib

English

Every Short x is a subsingleton, i.e., Short x has at most one element for any PGame x.

Русский

У каждого Short x есть не более одного элемента, то есть Short x — пододинственный.

LaTeX

$$$\forall x:\, \mathrm{PGame},\, \mathrm{Subsingleton}(\mathrm{Short}(x))$$$

Lean4

instance subsingleton_short (x : PGame) : Subsingleton (Short x) := by
  induction x with
  | mk xl xr xL xR =>
    constructor
    intro a b
    cases a; cases b
    congr!
      -- Porting note: We use `induction` to prove `subsingleton_short` instead of recursion.
      -- A proof using recursion generates a harder `decreasing_by` goal than in Lean 3 for some reason:

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