add_mem_Ioo_iff_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem add_mem_Ioo_iff_right : a + b ∈ Set.Ioo c d ↔ b ∈ Set.Ioo (c - a) (d - a) :=
  (and_congr sub_lt_iff_lt_add' lt_sub_iff_add_lt').symm

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