English
On a preconnected set s with two continuous functions f,g: s → α and endpoints mapped to v1,v2, the image of the open interval (v1,v2) lies in f''s.
Русский
На предсоединенном множестве s с двумя непрерывными функциями f,g: s → α и границами v1,v2, образ открытого интервала (v1,v2) лежит в f''(s).
LaTeX
$$$Ioo(v_1,v_2) \\subseteq f''(s).$$$
Lean4
theorem intermediate_value₂_eventually₂ {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [NeBot l₁] [NeBot l₂]
(hl₁ : l₁ ≤ 𝓟 s) (hl₂ : l₂ ≤ 𝓟 s) {f g : X → α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) (he₁ : f ≤ᶠ[l₁] g)
(he₂ : g ≤ᶠ[l₂] f) : ∃ x ∈ s, f x = g x :=
by
rw [continuousOn_iff_continuous_restrict] at hf hg
obtain ⟨b, h⟩ :=
@intermediate_value_univ₂_eventually₂ _ _ _ _ _ _ (Subtype.preconnectedSpace hs) _ _
(comap_coe_neBot_of_le_principal hl₁) (comap_coe_neBot_of_le_principal hl₂) _ _ hf hg (he₁.comap _) (he₂.comap _)
exact ⟨b, b.prop, h⟩
