internlm/Lean-Github huggingface dataset:
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
case hgt
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
⊢ ∃ t, (∀ x_1 ∈ t, x_1 ∈ Ioi x → x_1 ∈ ⇑ofDual ⁻¹' s) ∧ IsOpen t ∧ x ∈ t
Tactic:
rcases so (ofDual x) ⟨m.1, m.2.2, m.2.1⟩ with ⟨n, h, o, nx⟩
Proof state after:
case hgt.intro.intro.intro
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
⊢ ∃ t, (∀ x_1 ∈ t, x_1 ∈ Ioi x → x_1 ∈ ⇑ofDual ⁻¹' s) ∧ IsOpen t ∧ x ∈ t
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
case hgt.intro.intro.intro
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
⊢ ∃ t, (∀ x_1 ∈ t, x_1 ∈ Ioi x → x_1 ∈ ⇑ofDual ⁻¹' s) ∧ IsOpen t ∧ x ∈ t
Tactic:
use ofDual ⁻¹' n
Proof state after:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
⊢ (∀ x_1 ∈ ⇑ofDual ⁻¹' n, x_1 ∈ Ioi x → x_1 ∈ ⇑ofDual ⁻¹' s) ∧ IsOpen (⇑ofDual ⁻¹' n) ∧ x ∈ ⇑ofDual ⁻¹' n
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
⊢ (∀ x_1 ∈ ⇑ofDual ⁻¹' n, x_1 ∈ Ioi x → x_1 ∈ ⇑ofDual ⁻¹' s) ∧ IsOpen (⇑ofDual ⁻¹' n) ∧ x ∈ ⇑ofDual ⁻¹' n
Tactic:
refine ⟨?_, o.preimage continuous_ofDual, mem_preimage.mpr nx⟩
Proof state after:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
⊢ ∀ x_1 ∈ ⇑ofDual ⁻¹' n, x_1 ∈ Ioi x → x_1 ∈ ⇑ofDual ⁻¹' s
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
⊢ ∀ x_1 ∈ ⇑ofDual ⁻¹' n, x_1 ∈ Ioi x → x_1 ∈ ⇑ofDual ⁻¹' s
Tactic:
intro y m xy
Proof state after:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m✝ : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
y : Xᵒᵈ
m : y ∈ ⇑ofDual ⁻¹' n
xy : y ∈ Ioi x
⊢ y ∈ ⇑ofDual ⁻¹' s
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m✝ : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
y : Xᵒᵈ
m : y ∈ ⇑ofDual ⁻¹' n
xy : y ∈ Ioi x
⊢ y ∈ ⇑ofDual ⁻¹' s
Tactic:
simp only [Set.mem_Ioi] at xy
Proof state after:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m✝ : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
y : Xᵒᵈ
m : y ∈ ⇑ofDual ⁻¹' n
xy : x < y
⊢ y ∈ ⇑ofDual ⁻¹' s
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m✝ : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
y : Xᵒᵈ
m : y ∈ ⇑ofDual ⁻¹' n
xy : x < y
⊢ y ∈ ⇑ofDual ⁻¹' s
Tactic:
simp only [Set.mem_preimage]
Proof state after:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m✝ : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
y : Xᵒᵈ
m : y ∈ ⇑ofDual ⁻¹' n
xy : x < y
⊢ ofDual y ∈ s
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m✝ : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
h : ∀ x_1 ∈ n, x_1 ∈ Iio (ofDual x) → x_1 ∈ s
o : IsOpen n
nx : ofDual x ∈ n
y : Xᵒᵈ
m : y ∈ ⇑ofDual ⁻¹' n
xy : x < y
⊢ ofDual y ∈ s
Tactic:
simp only [Set.mem_Iio, Set.mem_preimage, OrderDual.ofDual_lt_ofDual] at h
Proof state after:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m✝ : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
o : IsOpen n
nx : ofDual x ∈ n
y : Xᵒᵈ
m : y ∈ ⇑ofDual ⁻¹' n
xy : x < y
h : ∀ x_1 ∈ n, x_1 < ofDual x → x_1 ∈ s
⊢ ofDual y ∈ s
Theorem: IsClosed.Icc_subset_of_forall_mem_nhds_within'
Proof state before:
case h
X : Type
inst✝³ : ConditionallyCompleteLinearOrder X
inst✝² : TopologicalSpace X
inst✝¹ : OrderTopology X
inst✝ : DenselyOrdered X
a b : X
s : Set X
sc : IsClosed (s ∩ Icc a b)
sb : b ∈ s
s' : Set Xᵒᵈ
hs' : ⇑ofDual ⁻¹' s = s'
x : Xᵒᵈ
so : ∀ (x : X), x ∈ s ∧ a < x ∧ x ≤ b → ∃ t, (∀ x_1 ∈ t, x_1 ∈ Iio x → x_1 ∈ s) ∧ IsOpen t ∧ x ∈ t
m✝ : x ∈ ⇑ofDual ⁻¹' s ∧ ofDual x ≤ b ∧ a < ofDual x
n : Set X
o : IsOpen n
nx : ofDual x ∈ n
y : Xᵒᵈ
m : y ∈ ⇑ofDual ⁻¹' n
xy : x < y
h : ∀ x_1 ∈ n, x_1 < ofDual x → x_1 ∈ s
⊢ ofDual y ∈ s
Tactic:
exact h _ m xy
Proof state after:
no goals
Theorem: IsPreconnected.sUnion_of_pairwise_exists_isPreconnected
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
⊢ IsPreconnected S.sUnion
Tactic:
refine isPreconnected_of_forall_pair fun x hx y hy ↦ ?_
Proof state after:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
Theorem: IsPreconnected.sUnion_of_pairwise_exists_isPreconnected
Proof state before:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
Tactic:
rcases mem_sUnion.1 hx with ⟨s, hs, hxs⟩
Proof state after:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
Theorem: IsPreconnected.sUnion_of_pairwise_exists_isPreconnected
Proof state before:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
Tactic:
rcases mem_sUnion.1 hy with ⟨t, ht, hyt⟩
Proof state after:
case intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
Theorem: IsPreconnected.sUnion_of_pairwise_exists_isPreconnected
Proof state before:
case intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
Tactic:
rcases eq_or_ne s t with rfl | hst
Proof state after:
case intro.intro.intro.intro.inl
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
ht : s ∈ S
hyt : y ∈ s
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t

case intro.intro.intro.intro.inr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
Theorem: IsPreconnected.sUnion_of_pairwise_exists_isPreconnected
Proof state before:
case intro.intro.intro.intro.inl
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
ht : s ∈ S
hyt : y ∈ s
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
Tactic:
exact ⟨s, subset_sUnion_of_mem hs, hxs, hyt, hSc s hs⟩
Proof state after:
no goals
Theorem: IsPreconnected.sUnion_of_pairwise_exists_isPreconnected
Proof state before:
case intro.intro.intro.intro.inr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
Tactic:
rcases h hs ht hst ⟨x, hxs⟩ ⟨y, hyt⟩ with ⟨u, huS, hsu, hut, hu⟩
Proof state after:
case intro.intro.intro.intro.inr.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
Theorem: IsPreconnected.sUnion_of_pairwise_exists_isPreconnected
Proof state before:
case intro.intro.intro.intro.inr.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ ∃ t ⊆ S.sUnion, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
Tactic:
refine ⟨s ∪ u ∪ t, ?_, ?_, ?_, ?_⟩
Proof state after:
case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_1
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ s ∪ u ∪ t ⊆ S.sUnion

case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ x ∈ s ∪ u ∪ t

case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_3
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ y ∈ s ∪ u ∪ t

case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_4
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ IsPreconnected (s ∪ u ∪ t)
Theorem: IsPreconnected.sUnion_of_pairwise_exists_isPreconnected
Proof state before:
case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_1
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ s ∪ u ∪ t ⊆ S.sUnion
Tactic:
simp [*, subset_sUnion_of_mem]
Proof state after:
no goals
Theorem: IsPreconnected.sUnion_of_pairwise_exists_isPreconnected
Proof state before:
case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ x ∈ s ∪ u ∪ t
Tactic:
simp [*]
Proof state after:
no goals
Theorem: IsPreconnected.sUnion_of_pairwise_exists_isPreconnected
Proof state before:
case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_3
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ y ∈ s ∪ u ∪ t
Tactic:
simp [*]
Proof state after:
no goals
Theorem: IsPreconnected.sUnion_of_pairwise_exists_isPreconnected
Proof state before:
case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_4
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ IsPreconnected (s ∪ u ∪ t)
Tactic:
refine ((hSc s hs).union' hsu hu).union' (hut.mono ?_) (hSc t ht)
Proof state after:
case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_4
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ u ∩ t ⊆ (s ∪ u) ∩ t
Theorem: IsPreconnected.sUnion_of_pairwise_exists_isPreconnected
Proof state before:
case intro.intro.intro.intro.inr.intro.intro.intro.intro.refine_4
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hSc : ∀ s ∈ S, IsPreconnected s
h :
  S.Pairwise fun s t => s.Nonempty → t.Nonempty → ∃ u ⊆ S.sUnion, (s ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
x : X
hx : x ∈ S.sUnion
y : X
hy : y ∈ S.sUnion
s : Set X
hs : s ∈ S
hxs : x ∈ s
t : Set X
ht : t ∈ S
hyt : y ∈ t
hst : s ≠ t
u : Set X
huS : u ⊆ S.sUnion
hsu : (s ∩ u).Nonempty
hut : (u ∩ t).Nonempty
hu : IsPreconnected u
⊢ u ∩ t ⊆ (s ∪ u) ∩ t
Tactic:
exact inter_subset_inter_left _ (subset_union_right _ _)
Proof state after:
no goals
Theorem: IsPreconnected.iUnion_of_pairwise_exists_isPreconnected
Proof state before:
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
s : ι → Set X
hsc : ∀ (i : ι), IsPreconnected (s i)
h :
  Pairwise fun i j =>
    (s i).Nonempty → (s j).Nonempty → ∃ u ⊆ ⋃ i, s i, (s i ∩ u).Nonempty ∧ (u ∩ s j).Nonempty ∧ IsPreconnected u
⊢ IsPreconnected (⋃ i, s i)
Tactic:
apply IsPreconnected.sUnion_of_pairwise_exists_isPreconnected (forall_mem_range.2 hsc)
Proof state after:
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
s : ι → Set X
hsc : ∀ (i : ι), IsPreconnected (s i)
h :
  Pairwise fun i j =>
    (s i).Nonempty → (s j).Nonempty → ∃ u ⊆ ⋃ i, s i, (s i ∩ u).Nonempty ∧ (u ∩ s j).Nonempty ∧ IsPreconnected u
⊢ (range fun i => s i).Pairwise fun s_1 t =>
    s_1.Nonempty →
      t.Nonempty → ∃ u ⊆ (range fun i => s i).sUnion, (s_1 ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
Theorem: IsPreconnected.iUnion_of_pairwise_exists_isPreconnected
Proof state before:
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
s : ι → Set X
hsc : ∀ (i : ι), IsPreconnected (s i)
h :
  Pairwise fun i j =>
    (s i).Nonempty → (s j).Nonempty → ∃ u ⊆ ⋃ i, s i, (s i ∩ u).Nonempty ∧ (u ∩ s j).Nonempty ∧ IsPreconnected u
⊢ (range fun i => s i).Pairwise fun s_1 t =>
    s_1.Nonempty →
      t.Nonempty → ∃ u ⊆ (range fun i => s i).sUnion, (s_1 ∩ u).Nonempty ∧ (u ∩ t).Nonempty ∧ IsPreconnected u
Tactic:
rintro _ ⟨i, rfl⟩ _ ⟨j, rfl⟩ hij
Proof state after:
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
s : ι → Set X
hsc : ∀ (i : ι), IsPreconnected (s i)
h :
  Pairwise fun i j =>
    (s i).Nonempty → (s j).Nonempty → ∃ u ⊆ ⋃ i, s i, (s i ∩ u).Nonempty ∧ (u ∩ s j).Nonempty ∧ IsPreconnected u
i j : ι
hij : (fun i => s i) i ≠ (fun i => s i) j
⊢ ((fun i => s i) i).Nonempty →
    ((fun i => s i) j).Nonempty →
      ∃ u ⊆ (range fun i => s i).sUnion,
        ((fun i => s i) i ∩ u).Nonempty ∧ (u ∩ (fun i => s i) j).Nonempty ∧ IsPreconnected u
Theorem: IsPreconnected.iUnion_of_pairwise_exists_isPreconnected
Proof state before:
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
s : ι → Set X
hsc : ∀ (i : ι), IsPreconnected (s i)
h :
  Pairwise fun i j =>
    (s i).Nonempty → (s j).Nonempty → ∃ u ⊆ ⋃ i, s i, (s i ∩ u).Nonempty ∧ (u ∩ s j).Nonempty ∧ IsPreconnected u
i j : ι
hij : (fun i => s i) i ≠ (fun i => s i) j
⊢ ((fun i => s i) i).Nonempty →
    ((fun i => s i) j).Nonempty →
      ∃ u ⊆ (range fun i => s i).sUnion,
        ((fun i => s i) i ∩ u).Nonempty ∧ (u ∩ (fun i => s i) j).Nonempty ∧ IsPreconnected u
Tactic:
exact h (ne_of_apply_ne s hij)
Proof state after:
no goals