Intervals cut out by finitely many affine inequalities

The elementary one-dimensional geometry used in the cell divergence theorem. Artificial outer endpoints allow a compactly supported field to be integrated without improper endpoint bookkeeping.

theorem LiebThirring.exists_strict_halfspace_of_face {ι : Type u_1} [Finite ι] (a b : ι → ℝ) (i : ι) (hi : a i ≠ 0) (hface : ∀ (j : ι), j ≠ i → b i / a i * a j < b j) : ∃ (t : ℝ), ∀ (j : ι), t * a j < b j

A transverse genuine facet has points of the open intersection beside it.

theorem LiebThirring.exists_truncated_halfspace_interval {ι : Type u_1} [Finite ι] (a b : ι → ℝ) {A B t₀ : ℝ} (hA : A < t₀) (hB : t₀ < B) (h₀ : ∀ (i : ι), t₀ * a i < b i) : ∃ (L : ℝ) (U : ℝ), A ≤ L ∧ L < t₀ ∧ t₀ < U ∧ U ≤ B ∧ (∀ (i : ι), 0 < a i → U ≤ b i / a i) ∧ (∀ (i : ι), a i < 0 → b i / a i ≤ L) ∧ (U = B ∨ ∃ (i : ι), 0 < a i ∧ U = b i / a i) ∧ (L = A ∨ ∃ (i : ι), a i < 0 ∧ L = b i / a i) ∧ ∀ (t : ℝ), (∀ (i : ι), t * a i < b i) ∧ A < t ∧ t < B ↔ L < t ∧ t < U

A nonempty slice of finitely many strict affine halfspaces, truncated to an interval containing a point of the slice, is itself an open interval.