theorem BNPair.image_mul_left_comp' {G : Type u_1} [Group G] (a b : G) (S : Set G) : (fun (x : G) => a * x) '' ((fun (x : G) => b * x) '' S) = (fun (x : G) => a * b * x) '' S

Composition of two left-multiplication maps on a subset $S$ collapses to multiplication by the product.

theorem BNPair.building_axiom_B2_cosets {G : Type u_1} [Group G] {B_idx : Type u_2} [DecidableEq B_idx] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (bd : bp.BruhatProperties) (ax : BNPairAxioms bp) (g h : G) (C : Set G) (hCg : C ∈ bp.translatedApartmentCosets g) (hCh : C ∈ bp.translatedApartmentCosets h) : ∃ (t : G), (∀ X ∈ bp.translatedApartmentCosets g, (fun (x : G) => t * x) '' X ∈ bp.translatedApartmentCosets h) ∧ (fun (x : G) => t * x) '' C = C

Building axiom (B2) at the coset level: if two translated apartments around $g, h$ share a chamber $C$, then there exists $t \in G$ carrying the $g$-apartment into the $h$-apartment while fixing $C$ setwise, i.e. $tC = C$ and $t \cdot \mathcal{A}_g \subseteq \mathcal{A}_h$.