internlm/Lean-Github huggingface dataset:
Theorem: IsPathConnected.of_frontier
Proof state before:
case right.intro.mk.intro.intro.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 : 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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
⊢ False
Tactic:
rcases lt_min_iff.mp zy1 with ⟨zy, z1⟩
Proof state after:
case right.intro.mk.intro.intro.intro.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 : 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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ False
Theorem: IsPathConnected.of_frontier
Proof state before:
case right.intro.mk.intro.intro.intro.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 : 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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ False
Tactic:
suffices h : z ∈ u by linarith [le_csSup bdd h]
Proof state after:
case right.intro.mk.intro.intro.intro.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 : 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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ z ∈ u
Theorem: IsPathConnected.of_frontier
Proof state before:
case right.intro.mk.intro.intro.intro.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 : 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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ z ∈ u
Tactic:
rw [← hu]
Proof state after:
case right.intro.mk.intro.intro.intro.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 : 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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ z ∈ Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a
Theorem: IsPathConnected.of_frontier
Proof state before:
case right.intro.mk.intro.intro.intro.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 : 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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ z ∈ Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a
Tactic:
refine ⟨⟨_root_.trans m.1 tz.le, z1.le⟩, ?_⟩
Proof state after:
case right.intro.mk.intro.intro.intro.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 : 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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ z ∈ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a
Theorem: IsPathConnected.of_frontier
Proof state before:
case right.intro.mk.intro.intro.intro.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 : 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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ z ∈ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a
Tactic:
simp only [mem_iInter₂, mem_Iic]
Proof state after:
case right.intro.mk.intro.intro.intro.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 : 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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ ∀ (i : ℝ), f (p.extend i) ∉ s → z ≤ i
Theorem: IsPathConnected.of_frontier
Proof state before:
case right.intro.mk.intro.intro.intro.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 : 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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
⊢ ∀ (i : ℝ), f (p.extend i) ∉ s → z ≤ i
Tactic:
intro w ws
Proof state after:
case right.intro.mk.intro.intro.intro.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 : 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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : f (p.extend w) ∉ s
⊢ z ≤ w
Theorem: IsPathConnected.of_frontier
Proof state before:
case right.intro.mk.intro.intro.intro.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 : 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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : f (p.extend w) ∉ s
⊢ z ≤ w
Tactic:
contrapose ws
Proof state after:
case right.intro.mk.intro.intro.intro.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 : 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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : ¬z ≤ w
⊢ ¬f (p.extend w) ∉ s
Theorem: IsPathConnected.of_frontier
Proof state before:
case right.intro.mk.intro.intro.intro.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 : 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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : ¬z ≤ w
⊢ ¬f (p.extend w) ∉ s
Tactic:
simp only [not_not, not_le] at ws ⊢
Proof state after:
case right.intro.mk.intro.intro.intro.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 : 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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
⊢ f (p.extend w) ∈ s
Theorem: IsPathConnected.of_frontier
Proof state before:
case right.intro.mk.intro.intro.intro.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 : 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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
⊢ f (p.extend w) ∈ s
Tactic:
by_cases xw : x < w
Proof state after:
case pos
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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
xw : x < w
⊢ f (p.extend w) ∈ s

case neg
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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
xw : ¬x < w
⊢ f (p.extend w) ∈ s
Theorem: IsPathConnected.of_frontier
Proof state before:
case pos
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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
xw : x < w
⊢ f (p.extend w) ∈ s

case neg
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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
xw : ¬x < w
⊢ f (p.extend w) ∈ s
Tactic:
refine interior_subset (h _ xw (_root_.trans ws zy))
Proof state after:
case neg
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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
xw : ¬x < w
⊢ f (p.extend w) ∈ s