Theorem: IsPreconnected.limits_atBot (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✝² : SemilatticeInf P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Iic a)
r : P → X
rc : Continuous r
⊢ IsPreconnected {x | MapClusterPt x atBot r}
Tactic:
set r' : Pᵒᵈ → X := r
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✝² : SemilatticeInf P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Iic a)
r : P → X
r' : Pᵒᵈ → X := r
rc : Continuous r'
⊢ IsPreconnected {x | MapClusterPt x atBot 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✝² : SemilatticeInf P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Iic a)
r : P → X
r' : Pᵒᵈ → X := r
rc : Continuous r'
⊢ IsPreconnected {x | MapClusterPt x atBot r'}
Tactic:
have rc' : Continuous r' := rc
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✝² : SemilatticeInf P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Iic a)
r : P → X
r' : Pᵒᵈ → X := r
rc : Continuous r'
rc' : Continuous r'
⊢ IsPreconnected {x | MapClusterPt x atBot 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✝² : SemilatticeInf P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Iic a)
r : P → X
r' : Pᵒᵈ → X := r
rc : Continuous r'
rc' : Continuous r'
⊢ IsPreconnected {x | MapClusterPt x atBot r'}
Tactic:
have p' : ∀ a : Pᵒᵈ, IsPreconnected (Ici a) := fun a ↦ p 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✝² : SemilatticeInf P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Iic a)
r : P → X
r' : Pᵒᵈ → X := r
rc : Continuous r'
rc' : Continuous r'
p' : ∀ (a : Pᵒᵈ), IsPreconnected (Ici a)
⊢ IsPreconnected {x | MapClusterPt x atBot 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✝² : SemilatticeInf P
inst✝¹ : TopologicalSpace P
inst✝ : Nonempty P
p : ∀ (a : P), IsPreconnected (Iic a)
r : P → X
r' : Pᵒᵈ → X := r
rc : Continuous r'
rc' : Continuous r'
p' : ∀ (a : Pᵒᵈ), IsPreconnected (Ici a)
⊢ IsPreconnected {x | MapClusterPt x atBot r'}
Tactic:
exact IsPreconnected.limits_atTop p' rc'
State after:
no goals