Is Orthochronous on connected component

lemma isOrthochronous_on_connected_component {Λ Λ' : LorentzGroup d}    (h : Λ' ∈ connectedComponent Λ) : IsOrthochronous Λ ↔ IsOrthochronous Λ' := by  obtain ⟨s, hs, hΛ'⟩ := h  let f : ContinuousMap s ℤ₂ := ContinuousMap.restrict s orthchroMap  haveI : PreconnectedSpace s := isPreconnected_iff_preconnectedSpace.mp hs.1  have h_eq : orthchroMap Λ = orthchroMap Λ' := by    apply IsPreconnected.subsingleton (isPreconnected_range f.continuous_toFun)    · exact Set.mem_range_self (⟨Λ, hs.2⟩ : {x : LorentzGroup d | x ∈ s})    · exact Set.mem_range_self (⟨Λ', hΛ'⟩ : {x : LorentzGroup d | x ∈ s})  exact isOrthochronous_iff_of_orthchroMap_eq h_eq