leftMoves_neg_cases — Mathlib

English

If for all i in x.RightMoves we have P(toLeftMovesNeg i), then for any k in (-x).LeftMoves we have P k.

Русский

Если для всех i ∈ x.RightMoves выполняется P(toLeftMovesNeg i), то для любого k ∈ (-x).LeftMoves верно P(k).

LaTeX

$$$$ (\forall i : x.RightMoves, P( toLeftMovesNeg(i) )) \Rightarrow P(k). $$$$

Lean4

theorem leftMoves_neg_cases {x : PGame} (k) {P : (-x).LeftMoves → Prop} (h : ∀ i, P <| toLeftMovesNeg i) : P k :=
  by
  rw [← toLeftMovesNeg.apply_symm_apply k]
  exact h _

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