forall_rightMoves_neg — Mathlib

English

For all i ∈ (-x).RightMoves, p i holds iff for all i ∈ x.LeftMoves, p (toRightMovesNeg i).

Русский

Для всех i ∈ (-x).RightMoves верно p i тогда и только тогда, когда для всех i ∈ x.LeftMoves верно p (toRightMovesNeg i).

LaTeX

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

Lean4

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

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