internlm/Lean-Github huggingface dataset:
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
p : Path x b
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
generalize hu : Icc (0 : ℝ) 1 ∩ ⋂ (a) (_ : f (p.extend a) ∉ s), Iic a = u
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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
⊢ 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
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
have bdd : BddAbove u := by rw [← hu, bddAbove_def]; use 1; intro t ⟨m, _⟩; exact m.2
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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
⊢ 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
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
have un : u.Nonempty := by
  rw [← hu]; use 0, left_mem_Icc.mpr zero_le_one; simp only [mem_iInter₂, mem_Iic]; intro a m
  contrapose m; simp only [not_not, p.extend_of_le_zero (not_le.mp m).le, 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
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
⊢ 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
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
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
have uc : IsClosed u := by
  rw [← hu]; apply isClosed_Icc.inter; apply isClosed_iInter; intro a; apply isClosed_iInter
  intro _; exact isClosed_Iic
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
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
⊢ 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
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
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
generalize ht : sSup u = t
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
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
⊢ 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
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
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
have tu : t ∈ u := by rw [← uc.closure_eq, ← ht]; exact csSup_mem_closure un bdd
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
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
⊢ 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
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
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
have m : t ∈ Icc (0 : ℝ) 1 := by rw [← hu] at tu; exact tu.1
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
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
⊢ 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
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
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
have lo : ∀ a, a ≤ t → f (p.extend a) ∈ s := by
  intro a h; contrapose h; simp only [not_le]
  replace h : ∀ᶠ b in 𝓝 a, f (p.extend b) ∉ s :=
    (fc.comp p.continuous_extend).continuousAt.eventually_mem (sc.isOpen_compl.mem_nhds h)
  simp only [← hu, mem_inter_iff, mem_iInter₂, mem_Iic] at tu ⊢
  rcases ((frequently_lt_nhds a).and_eventually h).exists with ⟨c, ca, cs⟩
  exact lt_of_le_of_lt (tu.2 c cs) ca
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
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
⊢ 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
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
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
by_cases t1 : t = 1
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
⊢ JoinedIn (f ⁻¹' s) b x

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
⊢ JoinedIn (f ⁻¹' s) b x
Theorem: IsPathConnected.of_frontier
Proof state before:
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
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
replace t1 : t < 1 := Ne.lt_of_le t1 m.2
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
⊢ JoinedIn (f ⁻¹' s) b x
Theorem: IsPathConnected.of_frontier
Proof state before:
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
ft : f (p ⟨t, m⟩) ∈ frontier s
⊢ JoinedIn (f ⁻¹' s) b x
Tactic:
refine ((pc.joinedIn _ ft b fb).mono (preimage_mono sc.frontier_subset)).symm.trans
  (JoinedIn.symm ?_)
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
ft : f (p ⟨t, m⟩) ∈ frontier s
⊢ JoinedIn (f ⁻¹' s) x (p ⟨t, m⟩)
Theorem: IsPathConnected.of_frontier
Proof state before:
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
ft : f (p ⟨t, m⟩) ∈ frontier s
⊢ JoinedIn (f ⁻¹' s) x (p ⟨t, m⟩)
Tactic:
generalize hq : (fun a : unitInterval ↦ p.extend (min a t)) = q
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
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
⊢ JoinedIn (f ⁻¹' s) x (p ⟨t, m⟩)
Theorem: IsPathConnected.of_frontier
Proof state before:
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
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
⊢ JoinedIn (f ⁻¹' s) x (p ⟨t, m⟩)
Tactic:
have qc : Continuous q := by
  rw [← hq]; exact p.continuous_extend.comp (continuous_subtype_val.min continuous_const)
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
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ JoinedIn (f ⁻¹' s) x (p ⟨t, m⟩)
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
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
⊢ BddAbove u
Tactic:
rw [← hu, bddAbove_def]
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
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
⊢ ∃ x_1, ∀ y ∈ Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a, y ≤ x_1
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
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
⊢ ∃ x_1, ∀ y ∈ Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a, y ≤ x_1
Tactic:
use 1
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
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
⊢ ∀ y ∈ Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a, y ≤ 1