theorem CellMulFinite.setMul_assoc {G : Type u_1} [Group G] (X Y Z : Set G) : setMul (setMul X Y) Z = setMul X (setMul Y Z)

Associativity of pointwise set multiplication: $(XY)Z = X(YZ)$.

theorem CellMulFinite.setMul_mono_left {G : Type u_1} [Group G] {X₁ X₂ Y : Set G} (h : X₁ ⊆ X₂) : setMul X₁ Y ⊆ setMul X₂ Y

Monotonicity of setMul in the left argument.

theorem CellMulFinite.setMul_mono_right {G : Type u_1} [Group G] {X Y₁ Y₂ : Set G} (h : Y₁ ⊆ Y₂) : setMul X Y₁ ⊆ setMul X Y₂

Monotonicity of setMul in the right argument.

theorem CellMulFinite.setMul_biUnion_left {G : Type u_1} [Group G] {ι : Type u_3} (A : ι → Set G) (B : Set G) (F : Finset ι) : setMul (⋃ i ∈ F, A i) B = ⋃ i ∈ F, setMul (A i) B

setMul distributes over a finite-indexed union on the left.

theorem CellMulFinite.bruhatCell_sub_setMul {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (w w' : M.Group) : bp.bruhatCell (w * w') ⊆ setMul (bp.bruhatCell w) (bp.bruhatCell w')

The cell of a product is contained in the product of cells: $C(ww') \subseteq C(w) \cdot C(w')$.

noncomputable def CellMulFinite.setMul_bruhatCell_simple_finset {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (_bp : BNPair G M) (_ax : BNPairAxioms _bp) (w : M.Group) (s : B_idx) : Finset M.Group

The (at most two-element) finset $\{ws, w\}$ covering $C(w) \cdot C(s)$ in the union of cells.

theorem CellMulFinite.setMul_bruhatCell_simple_subset {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (w : M.Group) (s : B_idx) : setMul (bp.bruhatCell w) (bp.bruhatCell (M.toCoxeterSystem.simple s)) ⊆ ⋃ u ∈ setMul_bruhatCell_simple_finset bp ax w s, bp.bruhatCell u

$C(w) \cdot C(s) \subseteq C(ws) \cup C(w)$: the product is covered by at most two cells.

theorem CellMulFinite.bruhatCell_mul_B_right {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) {w : M.Group} {g b : G} (hg : g ∈ bp.bruhatCell w) (hb : b ∈ bp.B) : g * b ∈ bp.bruhatCell w

Right $B$-absorption: $C(w) \cdot B \subseteq C(w)$.

theorem CellMulFinite.bruhatCell_one_sub_B {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) : bp.bruhatCell 1 ⊆ ↑bp.B

$C(1) \subseteq B$: the identity Bruhat cell is contained in $B$.

theorem CellMulFinite.setMul_bruhatCell_one {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (w : M.Group) : setMul (bp.bruhatCell w) (bp.bruhatCell 1) ⊆ bp.bruhatCell w

Right neutrality at the cell level: $C(w) \cdot C(1) \subseteq C(w)$.

theorem CellMulFinite.extend_finite_cover {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (w' : M.Group) (s : B_idx) (w₀ : M.Group) (us : Finset M.Group) (h_IH : setMul (bp.bruhatCell w₀) (bp.bruhatCell w') ⊆ ⋃ u ∈ us, bp.bruhatCell u) : ∃ (us' : Finset M.Group), setMul (bp.bruhatCell w₀) (bp.bruhatCell (w' * M.toCoxeterSystem.simple s)) ⊆ ⋃ u ∈ us', bp.bruhatCell u

Inductive step for cell-product finiteness: if $C(w_0) \cdot C(w')$ is covered by finitely many cells, then so is $C(w_0) \cdot C(w' s)$ for any simple $s$.

theorem CellMulFinite.cell_mul_finite_from_bnpair {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (w w' : M.Group) : ∃ (us : Finset M.Group), setMul (bp.bruhatCell w) (bp.bruhatCell w') ⊆ ⋃ u ∈ us, bp.bruhatCell u

Finiteness of cell products: for any $w, w' \in W$, the product $C(w) \cdot C(w')$ is contained in a finite union $\bigcup_{u \in U} C(u)$ of Bruhat cells.