Ioc_inl_inr

Mathlib.Data.Sum.Interval

URI: https://scilib.ai/kg/mathlib#Sum.Ioc_inl_inr

English

The half-open interval from a left-injection to a right-injection is empty: Ioc(inl a1, inr b2) = ∅.

Русский

Полуоткрытый интервал между левым и правым вложениями пуст.

LaTeX

$$$\mathrm{Ioc}(\mathrm{inl}(a_1),\mathrm{inr}(b_2)) = \emptyset$$$

Lean4

@[simp]
theorem Ioc_inl_inr : Ioc (inl a₁) (inr b₂) = ∅ :=
  rfl

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

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

Разделы

Аффилиация

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