exists_rightMoves_neg — Mathlib

English

There exists i ∈ (-x).RightMoves with p i, iff there exists i ∈ x.LeftMoves with p (toRightMovesNeg i).

Русский

Существует i ∈ (-x).RightMoves такое, что p i, эквивалентно существованию i ∈ x.LeftMoves с p (toRightMovesNeg i).

LaTeX

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

Lean4

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

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