add_mem_Ioc_iff_right — Mathlib

English

Let a,b,c,d be elements of an ordered additive group. Translating by a preserves membership in the interval Ioc: a + b ∈ Ioc(c,d) if and only if b ∈ Ioc(c − a, d − a).

Русский

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

LaTeX

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

Lean4

theorem add_mem_Ioc_iff_right : a + b ∈ Set.Ioc c d ↔ b ∈ Set.Ioc (c - a) (d - a) :=
  (and_congr sub_lt_iff_lt_add' le_sub_iff_add_le').symm

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