theorem holomorphicallyCompatible_restrOpen {X : Type u} [TopologicalSpace X] (e : OpenPartialHomeomorph X ℂ) {s : Set X} (hs : IsOpen s) : holomorphicallyCompatible (e.restrOpen s hs) e

Remark 1.2 (1): restricting a complex chart to an open subset of its source yields a complex chart holomorphically compatible with the original chart.

def ChartedSpace.IsComplexAtlas {X : Type u} [TopologicalSpace X] (c : ChartedSpace ℂ X) : Prop

A chosen charted-space structure on X is a complex atlas when its charts are pairwise holomorphically compatible. This is the source-facing compatibility condition from Definition 1.1 applied to a specific ChartedSpace value.

theorem ChartedSpace.isComplexAtlas_iff_analyticallyEquivalent_self {X : Type u} [TopologicalSpace X] (c : ChartedSpace ℂ X) : c.IsComplexAtlas ↔ analyticallyEquivalent c c

A chosen charted-space structure is a complex atlas exactly when it is analytically equivalent to itself.

theorem analyticallyEquivalent_refl {X : Type u} [TopologicalSpace X] {c : ChartedSpace ℂ X} (hc : c.IsComplexAtlas) : analyticallyEquivalent c c

Analytic equivalence of complex atlases is reflexive.

theorem analyticallyEquivalent_trans {X : Type u} [TopologicalSpace X] {c₁ c₂ c₃ : ChartedSpace ℂ X} (h₁₂ : analyticallyEquivalent c₁ c₂) (h₂₃ : analyticallyEquivalent c₂ c₃) : analyticallyEquivalent c₁ c₃

Analytic equivalence of complex atlases is transitive.

theorem analyticallyEquivalent_equivalence {X : Type u} [TopologicalSpace X] : Equivalence fun (c c' : { c : ChartedSpace ℂ X // c.IsComplexAtlas }) => analyticallyEquivalent ↑c ↑c'

Remark 1.2 (2): analytic equivalence of complex atlases is an equivalence relation.

@[implicit_reducible]

instance analyticallyEquivalentSetoid {X : Type u} [TopologicalSpace X] : Setoid { c : ChartedSpace ℂ X // c.IsComplexAtlas }

Analytic equivalence equips complex atlases on X with their canonical equivalence relation.