ofLine_mem — Mathlib

English

For a line-derived path, every value is attained by some point of the original line segment, i.e., the line path stays inside the image of f.

Русский

Образ пути, полученного из линии, состоит внутри образа функции f; каждый его член лежит в изображении f(I).

LaTeX

$$$\forall t,\; \mathrm{ofLine}(hf,h0,h1)(t) \in f(I)$$$

Lean4

theorem ofLine_mem {f : ℝ → X} (hf : ContinuousOn f I) (h₀ : f 0 = x) (h₁ : f 1 = y) :
    ∀ t, ofLine hf h₀ h₁ t ∈ f '' I := fun ⟨t, t_in⟩ => ⟨t, t_in, rfl⟩

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