Theorem: IsPathConnected.image_of_continuousOn (Ray/Misc/Connected.lean)

State before:
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
⊢ IsPathConnected (f '' s)
Tactic:
have uc : IsPathConnected (univ : Set s) := by
  convert sc.preimage_coe (subset_refl _); apply Set.ext; intro x
  simp only [mem_univ, true_iff_iff, mem_preimage, Subtype.mem]
State after:
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
⊢ IsPathConnected (f '' s)

State before:
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
⊢ IsPathConnected (f '' s)
Tactic:
have e : f '' s = s.restrict f '' univ := by
  apply Set.ext; intro y; constructor
  intro ⟨x, m, e⟩; use⟨x, m⟩, mem_univ _, e
  intro ⟨⟨x, m⟩, _, e⟩; use x, m, e
State after:
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
e : f '' s = s.restrict f '' univ
⊢ IsPathConnected (f '' s)

State before:
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
e : f '' s = s.restrict f '' univ
⊢ IsPathConnected (f '' s)
Tactic:
rw [e]
State after:
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
e : f '' s = s.restrict f '' univ
⊢ IsPathConnected (s.restrict f '' univ)

State before:
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
e : f '' s = s.restrict f '' univ
⊢ IsPathConnected (s.restrict f '' univ)
Tactic:
exact uc.image (continuousOn_iff_continuous_restrict.mp fc)
State after:
no goals

State before:
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
⊢ IsPathConnected univ
Tactic:
convert sc.preimage_coe (subset_refl _)
State after:
case h.e'_3
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
⊢ univ = Subtype.val ⁻¹' s

State before:
case h.e'_3
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
⊢ univ = Subtype.val ⁻¹' s
Tactic:
apply Set.ext
State after:
case h.e'_3.h
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
⊢ ∀ (x : ↑s), x ∈ univ ↔ x ∈ Subtype.val ⁻¹' s

State before:
case h.e'_3.h
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
⊢ ∀ (x : ↑s), x ∈ univ ↔ x ∈ Subtype.val ⁻¹' s
Tactic:
intro x
State after:
case h.e'_3.h
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
x : ↑s
⊢ x ∈ univ ↔ x ∈ Subtype.val ⁻¹' s

State before:
case h.e'_3.h
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
x : ↑s
⊢ x ∈ univ ↔ x ∈ Subtype.val ⁻¹' s
Tactic:
simp only [mem_univ, true_iff_iff, mem_preimage, Subtype.mem]
State after:
no goals

State before:
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
⊢ f '' s = s.restrict f '' univ
Tactic:
apply Set.ext
State after:
case h
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
⊢ ∀ (x : Y), x ∈ f '' s ↔ x ∈ s.restrict f '' univ

State before:
case h
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
⊢ ∀ (x : Y), x ∈ f '' s ↔ x ∈ s.restrict f '' univ
Tactic:
intro y
State after:
case h
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
y : Y
⊢ y ∈ f '' s ↔ y ∈ s.restrict f '' univ

State before:
case h
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
y : Y
⊢ y ∈ f '' s ↔ y ∈ s.restrict f '' univ
Tactic:
constructor
State after:
case h.mp
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
y : Y
⊢ y ∈ f '' s → y ∈ s.restrict f '' univ

case h.mpr
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
y : Y
⊢ y ∈ s.restrict f '' univ → y ∈ f '' s

State before:
case h.mp
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
y : Y
⊢ y ∈ f '' s → y ∈ s.restrict f '' univ

case h.mpr
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
y : Y
⊢ y ∈ s.restrict f '' univ → y ∈ f '' s
Tactic:
intro ⟨x, m, e⟩
State after:
case h.mp
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
y : Y
x : X
m : x ∈ s
e : f x = y
⊢ y ∈ s.restrict f '' univ

case h.mpr
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
y : Y
⊢ y ∈ s.restrict f '' univ → y ∈ f '' s

State before:
case h.mp
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
y : Y
x : X
m : x ∈ s
e : f x = y
⊢ y ∈ s.restrict f '' univ

case h.mpr
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
y : Y
⊢ y ∈ s.restrict f '' univ → y ∈ f '' s
Tactic:
use⟨x, m⟩, mem_univ _, e
State after:
case h.mpr
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
y : Y
⊢ y ∈ s.restrict f '' univ → y ∈ f '' s

State before:
case h.mpr
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
y : Y
⊢ y ∈ s.restrict f '' univ → y ∈ f '' s
Tactic:
intro ⟨⟨x, m⟩, _, e⟩
State after:
case h.mpr
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
y : Y
x : X
m : x ∈ s
left✝ : ⟨x, m⟩ ∈ univ
e : s.restrict f ⟨x, m⟩ = y
⊢ y ∈ f '' s

State before:
case h.mpr
X✝ : Type
inst✝⁶ : TopologicalSpace X✝
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
X Y : Type
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
sc : IsPathConnected s
f : X → Y
fc : ContinuousOn f s
uc : IsPathConnected univ
y : Y
x : X
m : x ∈ s
left✝ : ⟨x, m⟩ ∈ univ
e : s.restrict f ⟨x, m⟩ = y
⊢ y ∈ f '' s
Tactic:
use x, m, e
State after:
no goals