image_extend_of_subset — Mathlib

English

If I is contained in a subset s of the reals, then the image of γ.extend over s is exactly the image of γ.

Русский

Если единичный отрезок I содержится в подмножестве s множества вещественных чисел, то образ продолжения γ.extend по s совпадает с образом γ.

LaTeX

$$$\gamma.extend '' s = \mathrm{range}(\gamma)$ whenever $I \subseteq s$.$$

Lean4

theorem image_extend_of_subset (γ : Path x y) {s : Set ℝ} (h : I ⊆ s) : γ.extend '' s = range γ :=
  (γ.extend_range ▸ image_subset_range _ _).antisymm <| range_subset_iff.mpr <| fun t ↦ ⟨t, h t.2, extend_extends' _ _⟩

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