X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst✝ : NeBot l
hl : l ≤ 𝓟 s
f g : X → α
hf : Continuous (restrict s f)
hg : Continuous (restrict s g)
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
⊢ ∃ x, x ∈ s ∧ f x = g x
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst✝ : NeBot l
hl : l ≤ 𝓟 s
f g : X → α
hf : ContinuousOn f s
hg : ContinuousOn g s
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
⊢ ∃ x, x ∈ s ∧ f x = g x
rw [continuousOn_iff_continuous_restrict] at hf hg
case intro
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst✝ : NeBot l
hl : l ≤ 𝓟 s
f g : X → α
hf : Continuous (restrict s f)
hg : Continuous (restrict s g)
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
b : ↑s
h : restrict s f b = restrict s g b
⊢ ∃ x, x ∈ s ∧ f x = g x
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst✝ : NeBot l
hl : l ≤ 𝓟 s
f g : X → α
hf : Continuous (restrict s f)
hg : Continuous (restrict s g)
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
⊢ ∃ x, x ∈ s ∧ f x = g x
obtain ⟨b, h⟩ :=
  @intermediate_value_univ₂_eventually₁ _ _ _ _ _ _ (Subtype.preconnectedSpace hs) ⟨a, ha⟩ _
    (comap_coe_neBot_of_le_principal hl) _ _ hf hg ha' (he.comap _)
no goals
case intro
X : Type u
α : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
s : Set X
hs : IsPreconnected s
a : X
l : Filter X
ha : a ∈ s
inst✝ : NeBot l
hl : l ≤ 𝓟 s
f g : X → α
hf : Continuous (restrict s f)
hg : Continuous (restrict s g)
ha' : f a ≤ g a
he : g ≤ᶠ[l] f
b : ↑s
h : restrict s f b = restrict s g b
⊢ ∃ x, x ∈ s ∧ f x = g x
exact ⟨b, b.prop, h⟩