def IsUpperTriangularModM_Isometry (C : DVRContext) (g : Fin C.n → Fin C.n → C.𝔬) : Prop

An $n \times n$ matrix over $\mathfrak{o}$ is upper-triangular modulo $\mathfrak{m}$ if every strictly-below-diagonal entry is divisible by the uniformizer $\pi$.

def IsCongruentToIdentity_Isometry (C : DVRContext) (g : Fin C.n → Fin C.n → C.𝔬) : Prop

A matrix is congruent to the identity modulo $\mathfrak{m}$ if each entry differs from the corresponding entry of the identity matrix by a multiple of the uniformizer $\pi$.

theorem isometry_congruent_to_identity_is_upper_tri (C : DVRContext) (g : Fin C.n → Fin C.n → C.𝔬) (hg : IsCongruentToIdentity_Isometry C g) : IsUpperTriangularModM_Isometry C g

A matrix congruent to the identity mod $\mathfrak{m}$ is in particular upper-triangular mod $\mathfrak{m}$: the off-diagonal entries reduce to zero $\bmod\ \mathfrak{m}$, hence are multiples of $\pi$.

def IwahoriSubgroup_Alternating (C : DVRContext) : Set (Fin C.n → Fin C.n → C.𝔬)

The Iwahori subgroup of the isometry group in the alternating-form setting: matrices that are upper-triangular modulo $\mathfrak{m}$.

def Isometry.ParahoricSubgroup (C : DVRContext) (chain : ℤ → C.OLattice) (J : Set ℤ) : Set (Fin C.n → Fin C.n → C.𝔬)

The parahoric subgroup associated to a lattice chain and an index set $J$: matrices preserving each $\mathfrak{o}$-lattice $\Lambda_j$ for $j \in J$.

theorem open_plus_decomp_closed_isometry {α : Type u_1} [TopologicalSpace α] (B : Set α) (_hopen : IsOpen B) (hdecomp : ∃ (I : Type u_2) (cells : I → Set α), (∀ (i : I), IsOpen (cells i)) ∧ Set.univ = ⋃ (i : I), cells i ∧ (∀ (i j : I), i ≠ j → Disjoint (cells i) (cells j)) ∧ ∃ (i₀ : I), cells i₀ = B) : IsClosed B

Abstract topology lemma: a set $B$ that is open and equals one cell of an open-cell partition is closed, because its complement is the open union of the other cells.

theorem closed_in_compact_isometry {α : Type u_1} [TopologicalSpace α] (B K : Set α) (hB_closed : IsClosed B) (hBK : B ⊆ K) (hK_compact : IsCompact K) : IsCompact B

Abstract topology lemma: a closed subset of a compact set is compact.

theorem maximal_apartment_system {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : Type u_2} (Δ : ThickBuildingData G X) (𝒜 : Set (Set X)) (h𝒜_stable : ∀ (g : G), ∀ A ∈ 𝒜, (fun (x : X) => Δ.act g x) '' A ∈ 𝒜) (hA₀_in_𝒜 : Δ.A₀ ∈ 𝒜) (h𝒜_sub_max : 𝒜 ⊆ Δ.maxAptSystem) : 𝒜 = Δ.maxAptSystem

For a thick building with a strongly transitive $G$-action, any $G$-stable apartment system $\mathcal{A}$ contained in the maximal apartment system and containing the reference apartment $A_0$ coincides with the maximal apartment system.