Remark after Lemma 1.1 — N(K₁ ∩ K₂, K₁ ∩ K₂) ⊆ N(K₁, K₂) ⊆ N(K₁ ∩ K₂, Q)

Proved

LovaszSchrijver.IntegerHull.N_inter_subset_N_subset_N_inter_Q

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

lift-and-projectmatrix-conep2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $K_1, K_2 \subseteq Q$ be closed convex cones in $\mathbb R^{n+1}$ . Then

N(K_1 \cap K_2, K_1 \cap K_2) \subseteq N(K_1, K_2) \subseteq N(K_1 \cap K_2, Q).

The paper introduces it with "It is easy to see that"; it explains why it suffices to study the two special choices $K_1 = K_2 = K$ and $K_1 = K$ , $K_2 = Q$ , and the operator $N(K) = N(K, Q)$ that is iterated in Theorem 1.4.

Formalization Note The right-hand inclusion uses the rewriting (iii′), which needs $K_i^{**} = K_i$ ; the paper tacitly takes the cones closed (polyhedral in all its applications), and both cones are assumed closed.

Preamble

import Mathlib
import Definitions.Def_LovaszSchrijver_IntegerHull_Basic
import Definitions.Def_LovaszSchrijver_IntegerHull_MatrixCone
open Matrix Pointwise

Formal statement

namespace LovaszSchrijver.IntegerHull

theorem N_inter_subset_N_subset_N_inter_Q {ι : Type} [Fintype ι] [DecidableEq ι]
    (K₁ K₂ : Set (Option ι → ℝ)) (hK₁ : IsConvexCone K₁) (hK₂ : IsConvexCone K₂)
    (hK₁c : IsClosed K₁) (hK₂c : IsClosed K₂) (hK₁Q : K₁ ⊆ Q) (hK₂Q : K₂ ⊆ Q) :
    N (K₁ ∩ K₂) (K₁ ∩ K₂) ⊆ N K₁ K₂ ∧ N K₁ K₂ ⊆ N (K₁ ∩ K₂) Q := by sorry

end LovaszSchrijver.IntegerHull

Source

Lovász and Schrijver, Cones of matrices and set-functions and 0–1 optimization, SIAM J. Optim. 1(2) (1991), p. 170, Section 1.a (display after Lemma 1.1)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $\iota$ be a finite type with decidable equality, and let $V_\iota = \mathbb{R}^{\{0\}\sqcup\iota}$ . Let $Q$ be the set of finite nonnegative combinations of vectors with all coordinates in $\{0,1\}$ and $0$ -th coordinate $1$ .

Let $K_1, K_2 \subseteq V_\iota$ each satisfy:

nonempty and closed under addition and nonnegative scaling;
topologically closed;
contained in $Q$ .

The statement asserts both inclusions

N(K_1\cap K_2,\ K_1\cap K_2) \ \subseteq\ N(K_1,K_2) \qquad\text{and}\qquad N(K_1,K_2) \ \subseteq\ N(K_1 \cap K_2,\ Q).

For sets $A, B$ , $N(A,B) = \{Y e_0 : Y \in M(A,B)\}$ is the set of $0$ -th columns of matrices $Y$ , indexed by $\{0\}\sqcup\iota$ , that satisfy:

$Y$ is symmetric;
$Y_{ii} = Y_{0i}$ for all $i \in \iota$ ;
$u^\top Y v \ge 0$ for all $u \in A^*$ and $v \in B^*$ , where $A^* = \{u : u^\top x \ge 0\ \forall x \in A\}$ .

Degenerate cases:

Intersection is $\{0\}$ . $K_1 \cap K_2$ always contains $0$ . If it equals $\{0\}$ , its dual cone is all of $V_\iota$ , and condition 3 must then hold for all $u$ (and, in the first set, for all $v$ ).
Hypotheses are satisfiable. $K_1 = K_2 = \{0\}$ meets them.
Empty $\iota$ . $V_\iota = \mathbb{R}$ , $Q = [0,\infty)$ , each $K_j$ is $\{0\}$ or $[0,\infty)$ , and $Y$ is a $1\times1$ matrix.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph