exists_leftMoves_neg — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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