The semidirect closure component of the Connes rigidity formalization.

theorem Connes.mem_vonNeumannClosure_iff_of_conj_image_eq {H : Type u_1} {J : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup J] [InnerProductSpace ℂ J] [CompleteSpace J] (U : H ≃ₗᵢ[ℂ] J) (S : Set (H →L[ℂ] H)) (T : Set (J →L[ℂ] J)) (hST : ⇑U.conjStarAlgEquiv '' S = T) (x : H →L[ℂ] H) : x ∈ vonNeumannClosure S ↔ U.conjStarAlgEquiv x ∈ vonNeumannClosure T

theorem Connes.vonNeumannClosure_eq_of_factor_generators {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S T : Set (H →L[ℂ] H)) (hsub : T ⊆ S) (hfactor : ∀ x ∈ S, ∃ a ∈ T, ∃ b ∈ T, x = a * b) : vonNeumannClosure S = vonNeumannClosure T

theorem Connes.semidirect_vonNeumannClosure_eq_inl_inr {A : Type u_1} {K : Type u_2} [Group A] [Group K] (φ : K →* MulAut A) : vonNeumannClosure (Set.range fun (x : A ⋊[φ] K) => ↑((leftRegularRepresentation (A ⋊[φ] K)) x)) = vonNeumannClosure ((Set.range fun (a : A) => ↑((leftRegularRepresentation (A ⋊[φ] K)) (SemidirectProduct.inl a))) ∪ Set.range fun (k : K) => ↑((leftRegularRepresentation (A ⋊[φ] K)) (SemidirectProduct.inr k)))