rightMoves_neg_cases — Mathlib

English

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

Русский

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

LaTeX

$$$$ (\forall i : x.LeftMoves, P( toRightMovesNeg(i) )) \Rightarrow P(k). $$$$

Lean4

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

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