def TitsCone.titsConeInterior {B : Type u_1} (M : CoxeterMatrix B) : Set (B → ℝ)

The interior of the Tits cone $\mathcal U^\circ$: points which are $\sigma^*_w$-images of strictly positive vectors $y > 0$, i.e. images of points in the open fundamental chamber.

theorem TitsCone.titsConeInterior_subset_titsCone {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : titsConeInterior M ⊆ titsConeSet M

The interior $\mathcal U^\circ$ is contained in $\mathcal U$.

theorem TitsCone.titsCone_interior_iff_open_chamber {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (x : B → ℝ) (hx : x ∈ titsConeSet M) : x ∈ titsConeInterior M ↔ ∀ (ws : List B), ∀ y ∈ titsFundamentalClosure M, x = wordAction M ws y → y ∈ titsFundamentalChamber M

Characterization of $\mathcal U^\circ$: a point $x \in \mathcal U$ lies in the interior iff every fundamental-domain representative of $x$ is in the open chamber $C$. This is essentially the rigidity of fundamental-domain uniqueness lifted to the interior.