intermediate_value_univ₂_eventually₂

English

On a preconnected space, if two continuous functions f,g: X → α satisfy f ≤ g eventually along l1 and g ≤ f eventually along l2, then there exists x with f(x) = g(x).

Русский

На предсоединенном пространстве, если непрерывные функции f,g удовлетворяют f ≤ g вдоль l1 и g ≤ f вдоль l2, то существует точка x такая, что f(x) = g(x).

LaTeX

$$$\\exists x, f(x) = g(x)$ under the stated hypotheses.$$

Lean4

theorem intermediate_value_univ₂_eventually₂ [PreconnectedSpace X] {l₁ l₂ : Filter X} [NeBot l₁] [NeBot l₂]
    {f g : X → α} (hf : Continuous f) (hg : Continuous g) (he₁ : f ≤ᶠ[l₁] g) (he₂ : g ≤ᶠ[l₂] f) : ∃ x, f x = g x :=
  let ⟨_, h₁⟩ := he₁.exists
  let ⟨_, h₂⟩ := he₂.exists
  intermediate_value_univ₂ hf hg h₁ h₂

Похожие утверждения