mem_image_Ioo — Mathlib

English

If x, y, z form a Sbtw triple, then the point y lies in the image of the open interval (0,1) under the lineMap from x to z.

Русский

Если x, y, z образуют тройку Sbtw, то точка y принадлежит образу линейного отображения lineMap(x,z) от интервала (0,1).

LaTeX

$$$y \in lineMap x z '' Set.Ioo (0 : R) 1$$$

Lean4

theorem mem_image_Ioo {x y z : P} (h : Sbtw R x y z) : y ∈ lineMap x z '' Set.Ioo (0 : R) 1 :=
  by
  rcases h with ⟨⟨t, ht, rfl⟩, hyx, hyz⟩
  rcases Set.eq_endpoints_or_mem_Ioo_of_mem_Icc ht with (rfl | rfl | ho)
  · exfalso
    exact hyx (lineMap_apply_zero _ _)
  · exfalso
    exact hyz (lineMap_apply_one _ _)
  · exact ⟨t, ho, rfl⟩

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