sbtw_one_zero_iff

Mathlib.Analysis.Convex.Between

URI: https://scilib.ai/kg/mathlib#sbtw_one_zero_iff

English

For x in R, Sbtw R 1 x 0 holds if and only if x ∈ (0,1).

Русский

Для x ∈ R, Sbtw R 1 x 0 верно тогда, когда x ∈ (0,1).

LaTeX

$$$$ \text{Sbtw } R 1 x 0 \iff x \in (0,1) $$$$

Lean4

@[simp]
theorem sbtw_one_zero_iff {x : R} : Sbtw R 1 x 0 ↔ x ∈ Set.Ioo (0 : R) 1 := by rw [sbtw_comm, sbtw_zero_one_iff]

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

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

Разделы

Аффилиация

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