mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard
verified publisher icon leanprover-community

feat(set_theory/game/pgame): notation and basic API for `P{x | y}`, `P{x |}`, `P{| x}`

Open vihdzp opened this issue 3 years ago • 1 comments

We introduce constructors for games P{x | y}, P{x |}, P{| x} and provide a basic API.

We also make 1 and star reducible, which allows us to remove redundant instances.

  • [x] depends on: #14658

Open in Gitpod

vihdzp avatar Jun 10 '22 00:06 vihdzp

This PR/issue depends on:

  • ~~leanprover-community/mathlib#14658~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Jun 15 '22 02:06 mathlib-dependent-issues-bot