Theorem: isOpen_noncritical (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)
⊢ IsOpen {p | ¬Critical (f p.1) p.2}
Tactic:
rw [isOpen_iff_eventually]
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)
⊢ ∀ x ∈ {p | ¬Critical (f p.1) p.2}, ∀ᶠ (y : ℂ × S) in 𝓝 x, y ∈ {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)
⊢ ∀ x ∈ {p | ¬Critical (f p.1) p.2}, ∀ᶠ (y : ℂ × S) in 𝓝 x, y ∈ {p | ¬Critical (f p.1) p.2}
Tactic:
intro ⟨c, z⟩ m
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 : ℂ
z : S
m : (c, z) ∈ {p | ¬Critical (f p.1) p.2}
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {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 : ℂ
z : S
m : (c, z) ∈ {p | ¬Critical (f p.1) p.2}
⊢ ∀ᶠ (y : ℂ × S) in 𝓝 (c, z), y ∈ {p | ¬Critical (f p.1) p.2}
Tactic:
exact mfderiv_ne_zero_eventually' (fa _) m
State after:
no goals