def GroupSetMul {G : Type u_1} [Mul G] (E F : Set G) : Set G

Set-theoretic product $EF = \{ ef : e \in E, f \in F \}$ in a multiplicative structure.

def GroupSetInv {G : Type u_1} [Inv G] (E : Set G) : Set G

Set-theoretic inverse $E^{-1} = \{e^{-1} : e \in E\}$.

structure BornologicalGroupData (G : Type u_1) [Group G] : Type u_1

Data of a bornology compatible with the group structure on $G$: a family of bounded sets closed under singletons, subsets, finite unions, group products, and inversion.

• bounded : Set (Set G)
• singleton_mem (x : G) : {x} ∈ self.bounded
• subset_mem (E : Set G) : E ∈ self.bounded → ∀ F ⊆ E, F ∈ self.bounded
• union_mem (E : Set G) : E ∈ self.bounded → ∀ F ∈ self.bounded, E ∪ F ∈ self.bounded
• mul_mem (E : Set G) : E ∈ self.bounded → ∀ F ∈ self.bounded, GroupSetMul E F ∈ self.bounded
• inv_mem (E : Set G) : E ∈ self.bounded → GroupSetInv E ∈ self.bounded

theorem BornologicalGroupData.empty_mem {G : Type u_1} [Group G] (bd : BornologicalGroupData G) : ∅ ∈ bd.bounded

The empty set is bounded.

def BornologicalGroupData.toBornology {G : Type u_1} [Group G] (bd : BornologicalGroupData G) : Bornology G

Underlying mathlib Bornology instance from BornologicalGroupData.

def BNPairBornology.IsBounded {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (E : Set G) : Prop

$E \subseteq G$ is bounded relative to a BN-pair if it is covered by finitely many Bruhat cells.

def BNPairBornology.boundedSets {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) : Set (Set G)

The collection of all sets bounded relative to a BN-pair.

theorem BNPairBornology.bruhatCell_isBounded {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (w : M.Group) : IsBounded bp (bp.bruhatCell w)

Each Bruhat cell is bounded.

theorem BNPairBornology.isBounded_subset {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) {E F : Set G} (hE : IsBounded bp E) (hFE : F ⊆ E) : IsBounded bp F

BN-pair boundedness is closed under taking subsets.

theorem BNPairBornology.isBounded_union {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) {E F : Set G} (hE : IsBounded bp E) (hF : IsBounded bp F) : IsBounded bp (E ∪ F)

BN-pair boundedness is closed under binary unions.

theorem BNPairBornology.singleton_isBounded {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (hcover : ∀ (g : G), ∃ (w : M.Group), g ∈ bp.bruhatCell w) (g : G) : IsBounded bp {g}

Singletons are bounded when the BN-pair Bruhat decomposition covers $G$.

theorem BNPairBornology.empty_isBounded {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) : IsBounded bp ∅

The empty set is BN-pair bounded.

def BNPairBornology.toBornologicalGroupData {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (hcover : ∀ (g : G), ∃ (w : M.Group), g ∈ bp.bruhatCell w) (hmul : ∀ E ∈ boundedSets bp, ∀ F ∈ boundedSets bp, GroupSetMul E F ∈ boundedSets bp) (hinv : ∀ E ∈ boundedSets bp, GroupSetInv E ∈ boundedSets bp) : BornologicalGroupData G

Promote a BN-pair with cover, product-closure, and inverse-closure to a BornologicalGroupData.

def BNPairBornology.toBornology {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (hcover : ∀ (g : G), ∃ (w : M.Group), g ∈ bp.bruhatCell w) : Bornology G

Bornology on $G$ induced by a BN-pair, given a Bruhat cover.

theorem BNPairBornology.isBounded_iff {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (hcover : ∀ (g : G), ∃ (w : M.Group), g ∈ bp.bruhatCell w) (E : Set G) : Bornology.IsBounded E ↔ IsBounded bp E

A set is bounded in the induced bornology iff it is BN-pair bounded.

def BNPairBornology.IsBoundedGeneralized {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} {Ω : Type u_3} (bp : BNPair G M) (extendedCells : Ω × M.Group → Set G) (E : Set G) : Prop

Generalized BN-pair boundedness using extended cells parameterized by $\Omega \times M.\mathrm{Group}$.