Misere combinatorial games.
class
MisereGames.Form.Ambient
{G : Type (u + 1)}
[Form G]
(IsAmbient : outParam (G → Prop))
extends MisereGames.Form.Hereditary IsAmbient, MisereGames.Form.ClosedUnderNeg IsAmbient :
Ambient predicates closed under the separator and downlink constructions.
- isAmbient_rootedAdjoint {r g : G} : IsAmbient r → IsAmbient g → IsAmbient (rootedAdjoint r g)
- isAmbient_rightSeparatorCandidate {r h x : G} : IsAmbient r → IsAmbient h → IsAmbient x → IsAmbient (Separation.rightSeparatorCandidate r h x)
- isAmbient_downlinkWitness {r g h : G} {x : ↑(moves Player.left g) → G} {y : ↑(moves Player.right h) → G} [Small.{u, u + 1} ↑(Separation.downlinkLeftSet r g h y)] [Small.{u, u + 1} ↑(Separation.downlinkRightSet r g h x)] : IsAmbient r → IsAmbient g → IsAmbient h → (∀ (gl : ↑(moves Player.left g)), IsAmbient (x gl)) → (∀ (hr : ↑(moves Player.right h)), IsAmbient (y hr)) → IsAmbient (Separation.downlinkWitness r g h x y)
Instances
theorem
MisereGames.Form.Ambient.isAmbient_leftSeparatorCandidate
{G : Type (u + 1)}
[Form G]
{IsAmbient : G → Prop}
[Ambient IsAmbient]
{r g x : G}
(h_root : IsAmbient r)
(hg : IsAmbient g)
(hx : IsAmbient x)
:
IsAmbient (Separation.leftSeparatorCandidate r g x)
The Left separator stays ambient: it is the conjugate of a right one.