Theorem: Separate.fc1 (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
w0m : w0 ∈ closedBall c0 r
⊢ ContinuousOn (fun z1 => f (w0, z1)) (closedBall c1 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
w0m : w0 ∈ closedBall c0 r
⊢ ContinuousOn (fun z1 => (w0, z1)) (closedBall c1 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
w0m : w0 ∈ closedBall c0 r
⊢ Set.MapsTo (fun z1 => (w0, z1)) (closedBall c1 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
w0m : w0 ∈ closedBall c0 r
⊢ ContinuousOn (fun z1 => (w0, z1)) (closedBall c1 r)
Tactic:
exact ContinuousOn.prod continuousOn_const continuousOn_id
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
w0m : w0 ∈ closedBall c0 r
⊢ Set.MapsTo (fun z1 => (w0, z1)) (closedBall c1 r) s
Tactic:
intro z1 z1m
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
w0m : w0 ∈ closedBall c0 r
z1 : ℂ
z1m : z1 ∈ closedBall c1 r
⊢ (fun z1 => (w0, z1)) z1 ∈ 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
w0m : w0 ∈ closedBall c0 r
z1 : ℂ
z1m : z1 ∈ closedBall c1 r
⊢ (fun z1 => (w0, z1)) z1 ∈ 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
w0m : w0 ∈ closedBall c0 r
z1 : ℂ
z1m : z1 ∈ closedBall c1 r
⊢ (fun z1 => (w0, z1)) z1 ∈ 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
w0m : w0 ∈ closedBall c0 r
z1 : ℂ
z1m : z1 ∈ closedBall c1 r
⊢ (fun z1 => (w0, z1)) z1 ∈ 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
w0m : w0 ∈ closedBall c0 r
z1 : ℂ
z1m : z1 ∈ closedBall c1 r
⊢ (fun z1 => (w0, z1)) z1 ∈ 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
w0m : w0 ∈ closedBall c0 r
z1 : ℂ
z1m : z1 ∈ closedBall c1 r
⊢ (fun z1 => (w0, z1)) z1 ∈ closedBall c0 r ×ˢ closedBall c1 r
Tactic:
exact Set.mem_prod.mpr ⟨w0m, z1m⟩
State after:
no goals