Icc_inr_inl

Mathlib.Data.Sum.Interval

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

English

The closed interval from a right-injection to a left-injection is empty: Icc(inr b1, inl a2) = ∅.

Русский

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

LaTeX

$$$\mathrm{Icc}(\mathrm{inr}(b_1),\mathrm{inl}(a_2)) = \emptyset$$$

Lean4

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

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

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

Разделы

Аффилиация

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