class Form.Ambient {G : Type (u + 1)} [Form G] (IsAmbient : outParam (G → Prop)) extends Form.Hereditary IsAmbient, Form.ClosedUnderNeg IsAmbient : Prop

• has_option {g g' : G} (h1 : IsAmbient g) (h2 : IsOption g' g) : IsAmbient g'
• neg_of {g : G} (h1 : IsAmbient g) : IsAmbient (-g)
• 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)

theorem 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.

instance Form.instAmbientIsLong {G : Type (u + 1)} [Form G] : Ambient IsLong

instance Form.instAmbientIsShort {G : Type (u + 1)} [Form G] : Ambient IsShort