forall_leftMoves_neg — Mathlib

English

For any x and any p, the statement holds that ∀ i ∈ (-x).LeftMoves, p i is equivalent to ∀ i ∈ x.RightMoves, p (toLeftMovesNeg i).

Русский

Для любого x и для любого p выполняется: ∀ i ∈ (-x).LeftMoves, p i эквивалентно ∀ i ∈ x.RightMoves, p (toLeftMovesNeg i).

LaTeX

$$$$ (\forall i : (-x).LeftMoves, p(i)) \iff (\forall i : x.RightMoves, p( toLeftMovesNeg(i) )). $$$$

Lean4

@[simp]
theorem forall_leftMoves_neg {x : PGame} {p : (-x).LeftMoves → Prop} :
    (∀ i : (-x).LeftMoves, p i) ↔ (∀ i : x.RightMoves, p (toLeftMovesNeg i)) :=
  toLeftMovesNeg.forall_congr_right.symm

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