Theorem: Separate.fc0 (Ray/Hartogs/Osgood.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
⊢ ContinuousOn (fun z0 => f (z0, w1)) (closedBall c0 r)
Tactic:
refine ContinuousOn.comp h.fc ?_ ?_
State after:
case refine_1
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
⊢ ContinuousOn (fun z0 => (z0, w1)) (closedBall c0 r)

case refine_2
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
⊢ Set.MapsTo (fun z0 => (z0, w1)) (closedBall c0 r) s

State before:
case refine_1
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
⊢ ContinuousOn (fun z0 => (z0, w1)) (closedBall c0 r)
Tactic:
exact ContinuousOn.prod continuousOn_id continuousOn_const
State after:
no goals

State before:
case refine_2
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
⊢ Set.MapsTo (fun z0 => (z0, w1)) (closedBall c0 r) s
Tactic:
intro z0 z0m
State after:
case refine_2
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
z0 : ℂ
z0m : z0 ∈ closedBall c0 r
⊢ (fun z0 => (z0, w1)) z0 ∈ s

State before:
case refine_2
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
z0 : ℂ
z0m : z0 ∈ closedBall c0 r
⊢ (fun z0 => (z0, w1)) z0 ∈ s
Tactic:
apply h.rs
State after:
case refine_2.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
z0 : ℂ
z0m : z0 ∈ closedBall c0 r
⊢ (fun z0 => (z0, w1)) z0 ∈ closedBall (c0, c1) r

State before:
case refine_2.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
z0 : ℂ
z0m : z0 ∈ closedBall c0 r
⊢ (fun z0 => (z0, w1)) z0 ∈ closedBall (c0, c1) r
Tactic:
rw [← closedBall_prod_same]
State after:
case refine_2.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
z0 : ℂ
z0m : z0 ∈ closedBall c0 r
⊢ (fun z0 => (z0, w1)) z0 ∈ closedBall c0 r ×ˢ closedBall c1 r

State before:
case refine_2.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ × ℂ → E
s : Set (ℂ × ℂ)
c0 c1 w0 w1 : ℂ
r b : ℝ
h : Separate f c0 c1 r b s
w1m : w1 ∈ ball c1 r
z0 : ℂ
z0m : z0 ∈ closedBall c0 r
⊢ (fun z0 => (z0, w1)) z0 ∈ closedBall c0 r ×ˢ closedBall c1 r
Tactic:
exact Set.mem_prod.mpr ⟨z0m, mem_open_closed w1m⟩
State after:
no goals