sub_mem_Ioc_iff_left — Mathlib

English

Let a,b,c,d ∈ α as above. Left translation by b preserves Ioc: a − b ∈ Ioc(c,d) ⇔ a ∈ Ioc(c + b, d + b).

Русский

Пусть a,b,c,d ∈ α. Сдвиг слева на b сохраняет Ioc: a − b ∈ Ioc(c, d) тогда и только тогда a ∈ Ioc(c + b, d + b).

LaTeX

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

Lean4

theorem sub_mem_Ioc_iff_left : a - b ∈ Set.Ioc c d ↔ a ∈ Set.Ioc (c + b) (d + b) :=
  and_congr lt_sub_iff_add_lt sub_le_iff_le_add

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