Theorem: IsPreconnected.limits_atTop (Ray/Misc/Connected.lean)

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Tactic:
generalize hs : (fun a ↦ closure (r '' Ici a)) = s
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
⊢ IsPreconnected {x | MapClusterPt x atTop r}

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Tactic:
have m : Antitone s := by
  intro a b ab; rw [← hs]; exact closure_mono (monotone_image (Ici_subset_Ici.mpr ab))
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
⊢ IsPreconnected {x | MapClusterPt x atTop r}

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Tactic:
have d : Directed Superset s := by
  intro a b; exact ⟨a ⊔ b, m le_sup_left, m le_sup_right⟩
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
⊢ IsPreconnected {x | MapClusterPt x atTop r}

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Tactic:
have p : ∀ a, IsPreconnected (s a) := by
  intro a; rw [← hs]; exact ((p _).image _ rc.continuousOn).closure
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
⊢ IsPreconnected {x | MapClusterPt x atTop r}

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Tactic:
have c : ∀ a, IsCompact (s a) := by
  intro a; rw [← hs]; exact isClosed_closure.isCompact
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
⊢ IsPreconnected {x | MapClusterPt x atTop r}

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Tactic:
have e : {x | MapClusterPt x atTop r} = ⋂ a, s a := by
  ext x
  simp only [mem_setOf, mem_iInter, mapClusterPt_iff, mem_closure_iff_nhds, Set.Nonempty,
    @forall_comm P, ← hs]
  apply forall_congr'; intro t
  simp only [@forall_comm P, mem_inter_iff, mem_image, mem_Ici, @and_comm (_ ∈ t),
    exists_exists_and_eq_and, Filter.frequently_atTop, exists_prop]
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
e : {x | MapClusterPt x atTop r} = ⋂ a, s a
⊢ IsPreconnected {x | MapClusterPt x atTop r}

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
e : {x | MapClusterPt x atTop r} = ⋂ a, s a
⊢ IsPreconnected {x | MapClusterPt x atTop r}
Tactic:
rw [e]
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
e : {x | MapClusterPt x atTop r} = ⋂ a, s a
⊢ IsPreconnected (⋂ a, s a)

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
e : {x | MapClusterPt x atTop r} = ⋂ a, s a
⊢ IsPreconnected (⋂ a, s a)
Tactic:
exact IsPreconnected.directed_iInter d p c
State after:
no goals

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
⊢ Antitone s
Tactic:
intro a b ab
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
a b : P
ab : a ≤ b
⊢ s b ≤ s a

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
a b : P
ab : a ≤ b
⊢ s b ≤ s a
Tactic:
rw [← hs]
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
a b : P
ab : a ≤ b
⊢ (fun a => closure (r '' Ici a)) b ≤ (fun a => closure (r '' Ici a)) a

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
a b : P
ab : a ≤ b
⊢ (fun a => closure (r '' Ici a)) b ≤ (fun a => closure (r '' Ici a)) a
Tactic:
exact closure_mono (monotone_image (Ici_subset_Ici.mpr ab))
State after:
no goals

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
⊢ Directed Superset s
Tactic:
intro a b
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
a b : P
⊢ ∃ z, s a ⊇ s z ∧ s b ⊇ s z

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
a b : P
⊢ ∃ z, s a ⊇ s z ∧ s b ⊇ s z
Tactic:
exact ⟨a ⊔ b, m le_sup_left, m le_sup_right⟩
State after:
no goals

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
⊢ ∀ (a : P), IsPreconnected (s a)
Tactic:
intro a
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
a : P
⊢ IsPreconnected (s a)

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
a : P
⊢ IsPreconnected (s a)
Tactic:
rw [← hs]
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
a : P
⊢ IsPreconnected ((fun a => closure (r '' Ici a)) a)

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
a : P
⊢ IsPreconnected ((fun a => closure (r '' Ici a)) a)
Tactic:
exact ((p _).image _ rc.continuousOn).closure
State after:
no goals

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
⊢ ∀ (a : P), IsCompact (s a)
Tactic:
intro a
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
a : P
⊢ IsCompact (s a)

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
a : P
⊢ IsCompact (s a)
Tactic:
rw [← hs]
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
a : P
⊢ IsCompact ((fun a => closure (r '' Ici a)) a)

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
a : P
⊢ IsCompact ((fun a => closure (r '' Ici a)) a)
Tactic:
exact isClosed_closure.isCompact
State after:
no goals

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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
⊢ {x | MapClusterPt x atTop r} = ⋂ a, s a
Tactic:
ext x
State after:
case h
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
x : X
⊢ x ∈ {x | MapClusterPt x atTop r} ↔ x ∈ ⋂ a, s a

State before:
case h
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
x : X
⊢ x ∈ {x | MapClusterPt x atTop r} ↔ x ∈ ⋂ a, s a
Tactic:
simp only [mem_setOf, mem_iInter, mapClusterPt_iff, mem_closure_iff_nhds, Set.Nonempty,
  @forall_comm P, ← hs]
State after:
case h
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
x : X
⊢ (∀ s ∈ 𝓝 x, ∃ᶠ (a : P) in atTop, r a ∈ s) ↔ ∀ b ∈ 𝓝 x, ∀ (a : P), ∃ x, x ∈ b ∩ r '' Ici a

State before:
case h
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
x : X
⊢ (∀ s ∈ 𝓝 x, ∃ᶠ (a : P) in atTop, r a ∈ s) ↔ ∀ b ∈ 𝓝 x, ∀ (a : P), ∃ x, x ∈ b ∩ r '' Ici a
Tactic:
apply forall_congr'
State after:
case h.h
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
x : X
⊢ ∀ (a : Set X), (a ∈ 𝓝 x → ∃ᶠ (a_2 : P) in atTop, r a_2 ∈ a) ↔ a ∈ 𝓝 x → ∀ (a_1 : P), ∃ x, x ∈ a ∩ r '' Ici a_1

State before:
case h.h
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
x : X
⊢ ∀ (a : Set X), (a ∈ 𝓝 x → ∃ᶠ (a_2 : P) in atTop, r a_2 ∈ a) ↔ a ∈ 𝓝 x → ∀ (a_1 : P), ∃ x, x ∈ a ∩ r '' Ici a_1
Tactic:
intro t
State after:
case h.h
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
x : X
t : Set X
⊢ (t ∈ 𝓝 x → ∃ᶠ (a : P) in atTop, r a ∈ t) ↔ t ∈ 𝓝 x → ∀ (a : P), ∃ x, x ∈ t ∩ r '' Ici a

State before:
case h.h
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
P : Type
inst✝² : SemilatticeSup P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p✝ : ∀ (a : P), IsPreconnected (Ici a)
r : P → X
rc : Continuous r
s : P → Set X
hs : (fun a => closure (r '' Ici a)) = s
m : Antitone s
d : Directed Superset s
p : ∀ (a : P), IsPreconnected (s a)
c : ∀ (a : P), IsCompact (s a)
x : X
t : Set X
⊢ (t ∈ 𝓝 x → ∃ᶠ (a : P) in atTop, r a ∈ t) ↔ t ∈ 𝓝 x → ∀ (a : P), ∃ x, x ∈ t ∩ r '' Ici a
Tactic:
simp only [@forall_comm P, mem_inter_iff, mem_image, mem_Ici, @and_comm (_ ∈ t),
  exists_exists_and_eq_and, Filter.frequently_atTop, exists_prop]
State after:
no goals