structure CartanDecomposition (𝔤 : Type u_1) [LieRing 𝔤] [LieAlgebra ℝ 𝔤] : Type u_1

• 𝔨 : LieSubalgebra ℝ 𝔤
• 𝔭 : Submodule ℝ 𝔤
• isCompl : IsCompl self.𝔨.toSubmodule self.𝔭
• bracket_𝔨_𝔭 (x y : 𝔤) : x ∈ self.𝔨 → y ∈ self.𝔭 → ⁅x, y⁆ ∈ self.𝔭
• bracket_𝔭_𝔭 (x y : 𝔤) : x ∈ self.𝔭 → y ∈ self.𝔭 → ⁅x, y⁆ ∈ self.𝔨.toSubmodule

structure IwasawaData (G : Type u_1) [Group G] [TopologicalSpace G] : Type u_1

• K : Subgroup G
• A : Subgroup G
• N : Subgroup G
• K_compact : CompactSpace ↥self.K
• A_comm (a b : ↥self.A) : a * b = b * a
• mul_surj (g : G) : ∃ (k : ↥self.K) (a : ↥self.A) (n : ↥self.N), g = ↑k * ↑a * ↑n
• mul_inj (k₁ k₂ : ↥self.K) (a₁ a₂ : ↥self.A) (n₁ n₂ : ↥self.N) : ↑k₁ * ↑a₁ * ↑n₁ = ↑k₂ * ↑a₂ * ↑n₂ → k₁ = k₂ ∧ a₁ = a₂ ∧ n₁ = n₂

theorem iwasawa_decomposition_exists (G : Type u_1) [Group G] [TopologicalSpace G] [ContinuousMul G] : Nonempty (IwasawaData G)