Theorem: SuperAtC.superNearC (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t : Set (ℂ × ℂ)
s : SuperAtC f d u
⊢ ∃ t, SuperNearC f d u t
Tactic:
rcases s.superNearC' isOpen_univ fun _ _ ↦ Set.mem_univ _ with ⟨t, _, s⟩
State after:
case intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s✝ : SuperAtC f d u
t : Set (ℂ × ℂ)
left✝ : t ⊆ univ
s : SuperNearC f d u t
⊢ ∃ t, SuperNearC f d u t

State before:
case intro.intro
f : ℂ → ℂ → ℂ
d : ℕ
u : Set ℂ
t✝ : Set (ℂ × ℂ)
s✝ : SuperAtC f d u
t : Set (ℂ × ℂ)
left✝ : t ⊆ univ
s : SuperNearC f d u t
⊢ ∃ t, SuperNearC f d u t
Tactic:
exact ⟨t, s⟩
State after:
no goals