sub_mem_Ioc_iff_right

Mathlib.Algebra.Order.Interval.Set.Group

URI: https://scilib.ai/kg/mathlib#Set.sub_mem_Ioc_iff_right

English

Let a,b,c,d ∈ α. The left translation by b gives: a − b ∈ Ioc c d ⇔ b ∈ Ico(a − d, a − c).

Русский

Пусть a,b,c,d ∈ α. Левый сдвиг на b: a − b ∈ Ioc(c,d) ⇔ b ∈ Ico(a − d, a − c).

LaTeX

$$$a - b \in \mathrm{Ioc}(c, d) \iff b \in \mathrm{Ico}(a - d, a - c)$$$

Lean4

theorem sub_mem_Ioc_iff_right : a - b ∈ Set.Ioc c d ↔ b ∈ Set.Ico (a - d) (a - c) :=
  and_comm.trans <| and_congr sub_le_comm lt_sub_comm

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

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

Разделы

Аффилиация

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