[GOAL]
𝕜 : Type u_1
inst✝³ : OrderedSemiring 𝕜
E : Type u_2
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : SMul 𝕜 E
S T : ProperCone 𝕜 E
h : S.toConvexCone = T.toConvexCone
⊢ S = T
[PROOFSTEP]
cases S
[GOAL]
case mk
𝕜 : Type u_1
inst✝³ : OrderedSemiring 𝕜
E : Type u_2
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : SMul 𝕜 E
T : ProperCone 𝕜 E
toConvexCone✝ : ConvexCone 𝕜 E
nonempty'✝ : Set.Nonempty toConvexCone✝.carrier
is_closed'✝ : IsClosed toConvexCone✝.carrier
h : { toConvexCone := toConvexCone✝, nonempty' := nonempty'✝, is_closed' := is_closed'✝ }.toConvexCone = T.toConvexCone
⊢ { toConvexCone := toConvexCone✝, nonempty' := nonempty'✝, is_closed' := is_closed'✝ } = T
[PROOFSTEP]
cases T
[GOAL]
case mk.mk
𝕜 : Type u_1
inst✝³ : OrderedSemiring 𝕜
E : Type u_2
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : SMul 𝕜 E
toConvexCone✝¹ : ConvexCone 𝕜 E
nonempty'✝¹ : Set.Nonempty toConvexCone✝¹.carrier
is_closed'✝¹ : IsClosed toConvexCone✝¹.carrier
toConvexCone✝ : ConvexCone 𝕜 E
nonempty'✝ : Set.Nonempty toConvexCone✝.carrier
is_closed'✝ : IsClosed toConvexCone✝.carrier
h :
  { toConvexCone := toConvexCone✝¹, nonempty' := nonempty'✝¹, is_closed' := is_closed'✝¹ }.toConvexCone =
    { toConvexCone := toConvexCone✝, nonempty' := nonempty'✝, is_closed' := is_closed'✝ }.toConvexCone
⊢ { toConvexCone := toConvexCone✝¹, nonempty' := nonempty'✝¹, is_closed' := is_closed'✝¹ } =
    { toConvexCone := toConvexCone✝, nonempty' := nonempty'✝, is_closed' := is_closed'✝ }
[PROOFSTEP]
congr
[GOAL]
𝕜 : Type u_1
inst✝⁴ : OrderedSemiring 𝕜
E : Type u_2
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : Module 𝕜 E
⊢ ConvexCone.Pointed 0.toConvexCone
[PROOFSTEP]
simp [ConvexCone.pointed_zero]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
K : ProperCone ℝ E
⊢ (map (ContinuousLinearMap.id ℝ E) K).toConvexCone = K.toConvexCone
[PROOFSTEP]
simpa using IsClosed.closure_eq K.isClosed
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
K : ProperCone ℝ E
y : E
⊢ y ∈ dual K ↔ ∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner x y
[PROOFSTEP]
rw [← mem_coe, coe_dual, mem_innerDualCone _ _]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
K : ProperCone ℝ E
y : E
⊢ (∀ (x : E), x ∈ ↑K → 0 ≤ inner x y) ↔ ∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner x y
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
f : E →L[ℝ] F
S : ProperCone ℝ F
⊢ 0 ∈ (ConvexCone.comap (↑f) S.toConvexCone).carrier
[PROOFSTEP]
simp only [ConvexCone.comap, mem_preimage, map_zero, SetLike.mem_coe, mem_coe]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
f : E →L[ℝ] F
S : ProperCone ℝ F
⊢ 0 ∈ S
[PROOFSTEP]
apply ProperCone.pointed
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
f : E →L[ℝ] F
S : ProperCone ℝ F
⊢ IsClosed (ConvexCone.comap (↑f) S.toConvexCone).carrier
[PROOFSTEP]
simp only [ConvexCone.comap, ContinuousLinearMap.coe_coe]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
f : E →L[ℝ] F
S : ProperCone ℝ F
⊢ IsClosed (↑f ⁻¹' ↑S.toConvexCone)
[PROOFSTEP]
apply IsClosed.preimage f.2 S.isClosed
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
G : Type u_3
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
g : F →L[ℝ] G
f : E →L[ℝ] F
S : ProperCone ℝ G
⊢ ↑(comap f (comap g S)) = ↑(comap (comp g f) S)
[PROOFSTEP]
congr
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
⊢ b ∈ map f K → ∀ (y : F), ↑(↑adjoint f) y ∈ dual K → 0 ≤ inner y b
[PROOFSTEP]
simp only [ProperCone.mem_map, ProperCone.mem_dual, adjoint_inner_right, ConvexCone.mem_closure,
  mem_closure_iff_seq_limit]
  -- there is a sequence `seq : ℕ → F` in the image of `f` that converges to `b`
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
⊢ (∃ x, (∀ (n : ℕ), x n ∈ ↑(ConvexCone.map (↑f) K.toConvexCone)) ∧ Tendsto x atTop (nhds b)) →
    ∀ (y : F), (∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner (↑f x) y) → 0 ≤ inner y b
[PROOFSTEP]
rintro ⟨seq, hmem, htends⟩ y hinner
[GOAL]
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : ℕ → F
hmem : ∀ (n : ℕ), seq n ∈ ↑(ConvexCone.map (↑f) K.toConvexCone)
htends : Tendsto seq atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner (↑f x) y
⊢ 0 ≤ inner y b
[PROOFSTEP]
suffices h : ∀ n, 0 ≤ ⟪y, seq n⟫_ℝ
[GOAL]
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : ℕ → F
hmem : ∀ (n : ℕ), seq n ∈ ↑(ConvexCone.map (↑f) K.toConvexCone)
htends : Tendsto seq atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner (↑f x) y
h : ∀ (n : ℕ), 0 ≤ inner y (seq n)
⊢ 0 ≤ inner y b
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : ℕ → F
hmem : ∀ (n : ℕ), seq n ∈ ↑(ConvexCone.map (↑f) K.toConvexCone)
htends : Tendsto seq atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner (↑f x) y
⊢ ∀ (n : ℕ), 0 ≤ inner y (seq n)
[PROOFSTEP]
exact ge_of_tendsto' (Continuous.seqContinuous (Continuous.inner (@continuous_const _ _ _ _ y) continuous_id) htends) h
[GOAL]
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : ℕ → F
hmem : ∀ (n : ℕ), seq n ∈ ↑(ConvexCone.map (↑f) K.toConvexCone)
htends : Tendsto seq atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner (↑f x) y
⊢ ∀ (n : ℕ), 0 ≤ inner y (seq n)
[PROOFSTEP]
intro n
[GOAL]
case h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : ℕ → F
hmem : ∀ (n : ℕ), seq n ∈ ↑(ConvexCone.map (↑f) K.toConvexCone)
htends : Tendsto seq atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner (↑f x) y
n : ℕ
⊢ 0 ≤ inner y (seq n)
[PROOFSTEP]
obtain ⟨_, h, hseq⟩ := hmem n
[GOAL]
case h.intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : ℕ → F
hmem : ∀ (n : ℕ), seq n ∈ ↑(ConvexCone.map (↑f) K.toConvexCone)
htends : Tendsto seq atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner (↑f x) y
n : ℕ
w✝ : E
h : w✝ ∈ ↑K.toConvexCone
hseq : ↑↑f w✝ = seq n
⊢ 0 ≤ inner y (seq n)
[PROOFSTEP]
simpa only [← hseq, real_inner_comm] using hinner h
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
⊢ (∀ (y : F), ↑(↑adjoint f) y ∈ dual K → 0 ≤ inner y b) → b ∈ map f K
[PROOFSTEP]
intro h
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ∀ (y : F), ↑(↑adjoint f) y ∈ dual K → 0 ≤ inner y b
⊢ b ∈ map f K
[PROOFSTEP]
contrapose! h
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
⊢ ∃ y, ↑(↑adjoint f) y ∈ dual K ∧ inner y b < 0
[PROOFSTEP]
obtain ⟨y, hxy, hyb⟩ :=
  ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem _ (K.map f).nonempty (K.map f).isClosed h
[GOAL]
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
y : F
hxy : ∀ (x : F), x ∈ (map f K).toConvexCone → 0 ≤ inner x y
hyb : inner y b < 0
⊢ ∃ y, ↑(↑adjoint f) y ∈ dual K ∧ inner y b < 0
[PROOFSTEP]
refine' ⟨y, _, hyb⟩
[GOAL]
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
y : F
hxy : ∀ (x : F), x ∈ (map f K).toConvexCone → 0 ≤ inner x y
hyb : inner y b < 0
⊢ ↑(↑adjoint f) y ∈ dual K
[PROOFSTEP]
simp_rw [ProperCone.mem_dual, adjoint_inner_right]
[GOAL]
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
y : F
hxy : ∀ (x : F), x ∈ (map f K).toConvexCone → 0 ≤ inner x y
hyb : inner y b < 0
⊢ ∀ ⦃x : E⦄, x ∈ K → 0 ≤ inner (↑f x) y
[PROOFSTEP]
intro x hxK
[GOAL]
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
y : F
hxy : ∀ (x : F), x ∈ (map f K).toConvexCone → 0 ≤ inner x y
hyb : inner y b < 0
x : E
hxK : x ∈ K
⊢ 0 ≤ inner (↑f x) y
[PROOFSTEP]
apply hxy (f x)
[GOAL]
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
y : F
hxy : ∀ (x : F), x ∈ (map f K).toConvexCone → 0 ≤ inner x y
hyb : inner y b < 0
x : E
hxK : x ∈ K
⊢ ↑f x ∈ (map f K).toConvexCone
[PROOFSTEP]
rw [ProperCone.coe_map]
[GOAL]
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
y : F
hxy : ∀ (x : F), x ∈ (map f K).toConvexCone → 0 ≤ inner x y
hyb : inner y b < 0
x : E
hxK : x ∈ K
⊢ ↑f x ∈ ConvexCone.closure (ConvexCone.map (↑f) K.toConvexCone)
[PROOFSTEP]
apply subset_closure
[GOAL]
case intro.intro.a
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
y : F
hxy : ∀ (x : F), x ∈ (map f K).toConvexCone → 0 ≤ inner x y
hyb : inner y b < 0
x : E
hxK : x ∈ K
⊢ ↑f x ∈ ↑(ConvexCone.map (↑f) K.toConvexCone)
[PROOFSTEP]
rw [SetLike.mem_coe, ConvexCone.mem_map]
[GOAL]
case intro.intro.a
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
y : F
hxy : ∀ (x : F), x ∈ (map f K).toConvexCone → 0 ≤ inner x y
hyb : inner y b < 0
x : E
hxK : x ∈ K
⊢ ∃ x_1, x_1 ∈ K.toConvexCone ∧ ↑↑f x_1 = ↑f x
[PROOFSTEP]
refine' ⟨x, hxK, by rw [coe_coe]⟩
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : ¬b ∈ map f K
y : F
hxy : ∀ (x : F), x ∈ (map f K).toConvexCone → 0 ≤ inner x y
hyb : inner y b < 0
x : E
hxK : x ∈ K
⊢ ↑↑f x = ↑f x
[PROOFSTEP]
rw [coe_coe]
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
disj : ¬b ∈ map f K
⊢ ∃ y, ↑(↑adjoint f) y ∈ dual K ∧ inner y b < 0
[PROOFSTEP]
contrapose! disj
[GOAL]
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
disj : ∀ (y : F), ↑(↑adjoint f) y ∈ dual K → 0 ≤ inner y b
⊢ b ∈ map f K
[PROOFSTEP]
rwa [K.hyperplane_separation]
