left_mem_image_Ici_of_right_ne

Mathlib.Analysis.Convex.Between

URI: https://scilib.ai/kg/mathlib#Wbtw.left_mem_image_Ici_of_right_ne

← MathLib Explorer

English

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

Русский

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

LaTeX

$$Wbtw(R,x,y,z) ∧ x ≠ y ⇒ x ∈ lineMap z y '' Ici(1)$$

Lean4

theorem left_mem_image_Ici_of_right_ne {x y z : P} (h : Wbtw R x y z) (hne : z ≠ y) :
    x ∈ lineMap z y '' Set.Ici (1 : R) :=
  h.symm.right_mem_image_Ici_of_left_ne hne

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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