intermediate_value_Ioc' — Mathlib

English

Let a ≤ b and f be continuous on [a, b]. Then Ico(f(b), f(a)) ⊆ f(Ico(a, b)).

Русский

Пусть a ≤ b и f непрерывна на [a, b]. Тогда Ico(f(b), f(a)) ⊆ f(Ico(a, b)).

LaTeX

$$$Ico\\left(f(b), f(a)\\right) \\subseteq f\\left(Ico(a, b)\\right)$$$

Lean4

theorem intermediate_value_Ioc' {a b : α} (hab : a ≤ b) {f : α → δ} (hf : ContinuousOn f (Icc a b)) :
    Ico (f b) (f a) ⊆ f '' Ioc a b :=
  Or.elim (eq_or_lt_of_le hab) (fun he _ h => absurd h.1 (not_le_of_gt (he ▸ h.2))) fun hlt =>
    @IsPreconnected.intermediate_value_Ico _ _ _ _ _ _ _ isPreconnected_Ioc _ _ ⟨hlt, refl b⟩
      (left_nhdsWithin_Ioc_neBot hlt) inf_le_right _ (hf.mono Ioc_subset_Icc_self) _
      ((hf.continuousWithinAt ⟨refl a, hab⟩).mono Ioc_subset_Icc_self)

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