Theorem: isClosed_critical (Ray/AnalyticManifold/OneDimension.lean)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
fa : Holomorphic (I.prod I) I (uncurry f)
⊢ IsClosed {p | Critical (f p.1) p.2}
Tactic:
have c := (isOpen_noncritical fa).isClosed_compl
State after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
fa : Holomorphic (I.prod I) I (uncurry f)
c : IsClosed {p | ¬Critical (f p.1) p.2}ᶜ
⊢ IsClosed {p | Critical (f p.1) p.2}

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
fa : Holomorphic (I.prod I) I (uncurry f)
c : IsClosed {p | ¬Critical (f p.1) p.2}ᶜ
⊢ IsClosed {p | Critical (f p.1) p.2}
Tactic:
simp only [compl_setOf, not_not] at c
State after:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
fa : Holomorphic (I.prod I) I (uncurry f)
c : IsClosed {a | Critical (f a.1) a.2}
⊢ IsClosed {p | Critical (f p.1) p.2}

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → S → T
fa : Holomorphic (I.prod I) I (uncurry f)
c : IsClosed {a | Critical (f a.1) a.2}
⊢ IsClosed {p | Critical (f p.1) p.2}
Tactic:
exact c
State after:
no goals