right_mem_image_Ioi

Mathlib.Analysis.Convex.Between

URI: https://scilib.ai/kg/mathlib#Sbtw.right_mem_image_Ioi

English

If Wbtw holds, then z lies in the image of lineMap x y with Ici.

Русский

Если выполняется Wbtw, то z лежит в образе lineMap x y с Ici.

LaTeX

$$Wbtw(R,x,y,z) → z ∈ lineMap x y '' Ici(1)$$

Lean4

theorem right_mem_image_Ioi {x y z : P} (h : Sbtw R x y z) : z ∈ lineMap x y '' Set.Ioi (1 : R) :=
  (sbtw_iff_left_ne_and_right_mem_image_Ioi.1 h).2

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru