internlm/Lean-Github huggingface dataset:
Theorem: IsPathConnected.image_of_continuousOn
Proof 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
Proof 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)
Theorem: IsPathConnected.image_of_continuousOn
Proof 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]
Proof 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)
Theorem: IsPathConnected.image_of_continuousOn
Proof 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)
Proof state after:
no goals
Theorem: IsPathConnected.image_of_continuousOn
Proof 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 _)
Proof 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
Theorem: IsPathConnected.image_of_continuousOn
Proof 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
Proof 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
Theorem: IsPathConnected.image_of_continuousOn
Proof 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
Proof 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
Theorem: IsPathConnected.image_of_continuousOn
Proof 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]
Proof state after:
no goals
Theorem: IsPathConnected.image_of_continuousOn
Proof 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
Proof 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
Theorem: IsPathConnected.image_of_continuousOn
Proof 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
Proof 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
Theorem: IsPathConnected.image_of_continuousOn
Proof 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
Proof 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
Theorem: IsPathConnected.image_of_continuousOn
Proof 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⟩
Proof 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
Theorem: IsPathConnected.image_of_continuousOn
Proof 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
Proof 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
Theorem: IsPathConnected.image_of_continuousOn
Proof 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⟩
Proof 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
Theorem: IsPathConnected.image_of_continuousOn
Proof 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
Proof state after:
no goals
Theorem: isPathConnected_sphere
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
z : ℂ
r : ℝ
r0 : 0 ≤ r
⊢ IsPathConnected (sphere z r)
Tactic:
rw [← abs_of_nonneg r0, ← image_circleMap_Ioc z r]
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
z : ℂ
r : ℝ
r0 : 0 ≤ r
⊢ IsPathConnected (circleMap z r '' Ioc 0 (2 * π))
Theorem: isPathConnected_sphere
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
z : ℂ
r : ℝ
r0 : 0 ≤ r
⊢ IsPathConnected (circleMap z r '' Ioc 0 (2 * π))
Tactic:
refine IsPathConnected.image ?_ (continuous_circleMap _ _)
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
z : ℂ
r : ℝ
r0 : 0 ≤ r
⊢ IsPathConnected (Ioc 0 (2 * π))
Theorem: isPathConnected_sphere
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
z : ℂ
r : ℝ
r0 : 0 ≤ r
⊢ IsPathConnected (Ioc 0 (2 * π))
Tactic:
exact (convex_Ioc 0 (2 * π)).isPathConnected (nonempty_Ioc.mpr Real.two_pi_pos)
Proof state after:
no goals
Theorem: IsPathConnected.of_frontier
Proof 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
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
⊢ IsPathConnected (f ⁻¹' s)
Tactic:
have pc' := pc
Proof 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
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
pc' : IsPathConnected (f ⁻¹' frontier s)
⊢ IsPathConnected (f ⁻¹' s)
Theorem: IsPathConnected.of_frontier
Proof 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
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
pc' : IsPathConnected (f ⁻¹' frontier s)
⊢ IsPathConnected (f ⁻¹' s)
Tactic:
rcases pc' with ⟨b, fb, j⟩
Proof state after:
case intro.intro
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
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : b ∈ f ⁻¹' frontier s
j : ∀ {y : X}, y ∈ f ⁻¹' frontier s → JoinedIn (f ⁻¹' frontier s) b y
⊢ IsPathConnected (f ⁻¹' s)
Theorem: IsPathConnected.of_frontier
Proof state before:
case intro.intro
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
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : b ∈ f ⁻¹' frontier s
j : ∀ {y : X}, y ∈ f ⁻¹' frontier s → JoinedIn (f ⁻¹' frontier s) b y
⊢ IsPathConnected (f ⁻¹' s)
Tactic:
use b
Proof 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
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : b ∈ f ⁻¹' frontier s
j : ∀ {y : X}, y ∈ f ⁻¹' frontier s → JoinedIn (f ⁻¹' frontier s) b y
⊢ b ∈ f ⁻¹' s ∧ ∀ {y : X}, y ∈ f ⁻¹' s → JoinedIn (f ⁻¹' s) b y
Theorem: IsPathConnected.of_frontier
Proof 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
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : b ∈ f ⁻¹' frontier s
j : ∀ {y : X}, y ∈ f ⁻¹' frontier s → JoinedIn (f ⁻¹' frontier s) b y
⊢ b ∈ f ⁻¹' s ∧ ∀ {y : X}, y ∈ f ⁻¹' s → JoinedIn (f ⁻¹' s) b y
Tactic:
simp only [mem_preimage, mem_singleton_iff] at fb j ⊢
Proof 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
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
⊢ f b ∈ s ∧ ∀ {y : X}, f y ∈ s → JoinedIn (f ⁻¹' s) b y
Theorem: IsPathConnected.of_frontier
Proof 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
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
⊢ f b ∈ s ∧ ∀ {y : X}, f y ∈ s → JoinedIn (f ⁻¹' s) b y
Tactic:
have bs : f b ∈ s := sc.frontier_subset fb
Proof 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
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
⊢ f b ∈ s ∧ ∀ {y : X}, f y ∈ s → JoinedIn (f ⁻¹' s) b y
Theorem: IsPathConnected.of_frontier
Proof 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
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
⊢ f b ∈ s ∧ ∀ {y : X}, f y ∈ s → JoinedIn (f ⁻¹' s) b y
Tactic:
use bs
Proof state after:
case right
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
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
⊢ ∀ {y : X}, f y ∈ s → JoinedIn (f ⁻¹' s) b y
Theorem: IsPathConnected.of_frontier
Proof state before:
case right
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
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
⊢ ∀ {y : X}, f y ∈ s → JoinedIn (f ⁻¹' s) b y
Tactic:
intro x fx
Proof state after:
case right
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
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
⊢ JoinedIn (f ⁻¹' s) b x
Theorem: IsPathConnected.of_frontier
Proof state before:
case right
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
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
have p := PathConnectedSpace.somePath x b
Proof state after:
case right
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
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
⊢ JoinedIn (f ⁻¹' s) b x