internlm/Lean-Github huggingface dataset:
Theorem: IsPreconnected.limits_Ioc
Proof state before:
case right
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m✝ : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c✝ : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x✝ : X
u : Set X
a✝ : u ∈ 𝓝 x✝
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
m : min w b ∈ Ioc a b
x : X
xu : x ∈ u
c : ℝ
cx : r c = x
ac : a < c
cw : c ≤ w
right✝ : c ≤ b
⊢ r c ∈ u
Tactic:
rwa [cx]
Proof state after:
no goals
Theorem: IsPreconnected.limits_Ioc
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
⊢ min w b ∈ Ioc a b
Tactic:
simp only [mem_Ioc]
Proof state after:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
⊢ a < min w b ∧ min w b ≤ b
Theorem: IsPreconnected.limits_Ioc
Proof state before:
X : Type
inst✝⁶ : TopologicalSpace X
I : Type
inst✝⁵ : TopologicalSpace I
inst✝⁴ : ConditionallyCompleteLinearOrder I
inst✝³ : DenselyOrdered I
inst✝² : OrderTopology I
inst✝¹ : CompactSpace X
inst✝ : T4Space X
r : ℝ → X
a b : ℝ
rc : ContinuousOn r (Ioc a b)
ab : a < b
s : ↑(Ioc a b) → Set X
hs : (fun t => closure (r '' Ioc a ↑t)) = s
n : Nonempty ↑(Ioc a b)
m : Monotone s
d : Directed Superset s
p : ∀ (t : ↑(Ioc a b)), IsPreconnected (s t)
c : ∀ (t : ↑(Ioc a b)), IsCompact (s t)
x : X
u : Set X
a✝ : u ∈ 𝓝 x
h : ∀ (a_1 : ↑(Ioc a b)), ∃ x ∈ u, x ∈ r '' Ioc a ↑a_1
v : Set ℝ
vm : v ∈ 𝓝[>] a
w : ℝ
wv : Ioc a w ⊆ v
wa : a < w
⊢ a < min w b ∧ min w b ≤ b
Tactic:
use lt_min wa ab, min_le_right _ _
Proof state after:
no goals
Theorem: IsPreconnected.relative_clopen
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
⊢ s ⊆ interior t
Tactic:
generalize hu : (fun x : s ↦ (x : X)) ⁻¹' t = u
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
⊢ s ⊆ interior t
Theorem: IsPreconnected.relative_clopen
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
⊢ s ⊆ interior t
Tactic:
have uo : IsOpen u := by
  rw [← subset_interior_iff_isOpen]; intro ⟨x, m⟩ h
  simp only [mem_preimage, Subtype.coe_mk, ← hu] at h
  have n := op ⟨m, h⟩
  simp only [mem_interior_iff_mem_nhds, preimage_coe_mem_nhds_subtype, Subtype.coe_mk,
    ← hu] at n ⊢
  exact nhdsWithin_le_nhds n
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ s ⊆ interior t
Theorem: IsPreconnected.relative_clopen
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ s ⊆ interior t
Tactic:
have uc : IsClosed u := by
  rw [← closure_eq_iff_isClosed]; refine subset_antisymm ?_ subset_closure
  rw [← hu]
  refine _root_.trans (continuous_subtype_val.closure_preimage_subset _) ?_
  intro ⟨x, m⟩ h; exact cl ⟨m, h⟩
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
⊢ s ⊆ interior t
Theorem: IsPreconnected.relative_clopen
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
⊢ s ⊆ interior t
Tactic:
have p : IsPreconnected (univ : Set s) := (Subtype.preconnectedSpace sp).isPreconnected_univ
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
⊢ s ⊆ interior t
Theorem: IsPreconnected.relative_clopen
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
⊢ s ⊆ interior t
Tactic:
cases' disjoint_or_subset_of_isClopen p ⟨uc, uo⟩ with h h
Proof state after:
case inl
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Disjoint univ u
⊢ s ⊆ interior t

case inr
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : univ ⊆ u
⊢ s ⊆ interior t
Theorem: IsPreconnected.relative_clopen
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
⊢ IsOpen u
Tactic:
rw [← subset_interior_iff_isOpen]
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
⊢ u ⊆ interior u
Theorem: IsPreconnected.relative_clopen
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
⊢ u ⊆ interior u
Tactic:
intro ⟨x, m⟩ h
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
x : X
m : x ∈ s
h : ⟨x, m⟩ ∈ u
⊢ ⟨x, m⟩ ∈ interior u
Theorem: IsPreconnected.relative_clopen
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
x : X
m : x ∈ s
h : ⟨x, m⟩ ∈ u
⊢ ⟨x, m⟩ ∈ interior u
Tactic:
simp only [mem_preimage, Subtype.coe_mk, ← hu] at h
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
x : X
m : x ∈ s
h : x ∈ t
⊢ ⟨x, m⟩ ∈ interior u
Theorem: IsPreconnected.relative_clopen
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
x : X
m : x ∈ s
h : x ∈ t
⊢ ⟨x, m⟩ ∈ interior u
Tactic:
have n := op ⟨m, h⟩
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
x : X
m : x ∈ s
h : x ∈ t
n : x ∈ interior t
⊢ ⟨x, m⟩ ∈ interior u
Theorem: IsPreconnected.relative_clopen
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
x : X
m : x ∈ s
h : x ∈ t
n : x ∈ interior t
⊢ ⟨x, m⟩ ∈ interior u
Tactic:
simp only [mem_interior_iff_mem_nhds, preimage_coe_mem_nhds_subtype, Subtype.coe_mk,
  ← hu] at n ⊢
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
x : X
m : x ∈ s
h : x ∈ t
n : t ∈ 𝓝 x
⊢ t ∈ 𝓝[s] x
Theorem: IsPreconnected.relative_clopen
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
x : X
m : x ∈ s
h : x ∈ t
n : t ∈ 𝓝 x
⊢ t ∈ 𝓝[s] x
Tactic:
exact nhdsWithin_le_nhds n
Proof state after:
no goals
Theorem: IsPreconnected.relative_clopen
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ IsClosed u
Tactic:
rw [← closure_eq_iff_isClosed]
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ closure u = u
Theorem: IsPreconnected.relative_clopen
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ closure u = u
Tactic:
refine subset_antisymm ?_ subset_closure
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ closure u ⊆ u
Theorem: IsPreconnected.relative_clopen
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ closure u ⊆ u
Tactic:
rw [← hu]
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ closure ((fun x => ↑x) ⁻¹' t) ⊆ (fun x => ↑x) ⁻¹' t
Theorem: IsPreconnected.relative_clopen
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ closure ((fun x => ↑x) ⁻¹' t) ⊆ (fun x => ↑x) ⁻¹' t
Tactic:
refine _root_.trans (continuous_subtype_val.closure_preimage_subset _) ?_
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ Subtype.val ⁻¹' closure t ⊆ (fun x => ↑x) ⁻¹' t
Theorem: IsPreconnected.relative_clopen
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
⊢ Subtype.val ⁻¹' closure t ⊆ (fun x => ↑x) ⁻¹' t
Tactic:
intro ⟨x, m⟩ h
Proof state after:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
x : X
m : x ∈ s
h : ⟨x, m⟩ ∈ Subtype.val ⁻¹' closure t
⊢ ⟨x, m⟩ ∈ (fun x => ↑x) ⁻¹' t
Theorem: IsPreconnected.relative_clopen
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
x : X
m : x ∈ s
h : ⟨x, m⟩ ∈ Subtype.val ⁻¹' closure t
⊢ ⟨x, m⟩ ∈ (fun x => ↑x) ⁻¹' t
Tactic:
exact cl ⟨m, h⟩
Proof state after:
no goals
Theorem: IsPreconnected.relative_clopen
Proof state before:
case inl
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Disjoint univ u
⊢ s ⊆ interior t
Tactic:
simp only [univ_disjoint, preimage_eq_empty_iff, Subtype.range_coe, ← hu] at h
Proof state after:
case inl
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Disjoint t s
⊢ s ⊆ interior t
Theorem: IsPreconnected.relative_clopen
Proof state before:
case inl
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Disjoint t s
⊢ s ⊆ interior t
Tactic:
exfalso
Proof state after:
case inl
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Disjoint t s
⊢ False
Theorem: IsPreconnected.relative_clopen
Proof state before:
case inl
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Disjoint t s
⊢ False
Tactic:
exact ne.not_disjoint h.symm
Proof state after:
no goals
Theorem: IsPreconnected.relative_clopen
Proof state before:
case inr
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : univ ⊆ u
⊢ s ⊆ interior t
Tactic:
rw [← Subtype.coe_preimage_self, ← hu, preimage_subset_preimage_iff] at h
Proof state after:
case inr
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : s ⊆ t
⊢ s ⊆ interior t

case inr
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Subtype.val ⁻¹' s ⊆ (fun x => ↑x) ⁻¹' t
⊢ s ⊆ range Subtype.val
Theorem: IsPreconnected.relative_clopen
Proof state before:
case inr
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : s ⊆ t
⊢ s ⊆ interior t

case inr
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Subtype.val ⁻¹' s ⊆ (fun x => ↑x) ⁻¹' t
⊢ s ⊆ range Subtype.val
Tactic:
exact _root_.trans (subset_inter (subset_refl _) h) op
Proof state after:
case inr
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Subtype.val ⁻¹' s ⊆ (fun x => ↑x) ⁻¹' t
⊢ s ⊆ range Subtype.val
Theorem: IsPreconnected.relative_clopen
Proof state before:
case inr
X : Type
inst✝⁴ : TopologicalSpace X
I : Type
inst✝³ : TopologicalSpace I
inst✝² : ConditionallyCompleteLinearOrder I
inst✝¹ : DenselyOrdered I
inst✝ : OrderTopology I
s t : Set X
sp : IsPreconnected s
ne : (s ∩ t).Nonempty
op : s ∩ t ⊆ interior t
cl : s ∩ closure t ⊆ t
u : Set ↑s
hu : (fun x => ↑x) ⁻¹' t = u
uo : IsOpen u
uc : IsClosed u
p : IsPreconnected univ
h : Subtype.val ⁻¹' s ⊆ (fun x => ↑x) ⁻¹' t
⊢ s ⊆ range Subtype.val
Tactic:
simp only [Subtype.range_coe, subset_refl]
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 (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]
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
⊢ IsPathConnected (f '' s)